# HG changeset patch
# User paulson
# Date 927277127 -7200
# Node ID 629b4b3d5beefe2891d6af61406f7e289e13d216
# Parent  62d1e642da30e3ff683174f491c126e35cebbf3d
made definition more readable

diff -r 62d1e642da30 -r 629b4b3d5bee src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Fri May 21 10:56:46 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy	Fri May 21 10:58:47 1999 +0200
@@ -16,7 +16,7 @@
     "extend_set h A == h `` (A Times UNIV)"
 
   extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c * 'c) set"
-    "extend_act h == (%act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))})"
+    "extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
 
   extend :: "['a*'b => 'c, 'a program] => 'c program"
     "extend h F == mk_program (extend_set h (Init F),