Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/SubstAx.thy
changeset 5648 fe887910e32e
parent 5620 3ac11c4af76a
child 6536 281d44905cab 
--- a/src/HOL/UNITY/SubstAx.thy	Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Thu Oct 15 11:35:07 1998 +0200
@@ -10,9 +10,7 @@
 
 constdefs
 
-   LeadsTo :: "['a program, 'a set, 'a set] => bool"
-    "LeadsTo F A B ==
-		 leadsTo (Acts F)
-                         (reachable F  Int  A)
-  		         (reachable F  Int  B)"
+   LeadsTo :: "['a set, 'a set] => 'a program set"
+    "LeadsTo A B == {F. F : leadsTo (reachable F  Int  A)
+	   	                    (reachable F  Int  B)}"
 end
isabelle