made definition more readable
authorpaulson
Fri, 21 May 1999 10:58:47 +0200
changeset 6677 629b4b3d5bee
parent 6676 62d1e642da30
child 6678 d83f27b03529
made definition more readable
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),