src/HOL/UNITY/SubstAx.thy
changeset 5620 3ac11c4af76a
parent 5313 1861a564d7e2
child 5648 fe887910e32e
--- a/src/HOL/UNITY/SubstAx.thy	Wed Oct 07 10:31:30 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Wed Oct 07 10:32:00 1998 +0200
@@ -11,8 +11,8 @@
 constdefs
 
    LeadsTo :: "['a program, 'a set, 'a set] => bool"
-    "LeadsTo prg A B ==
-		 leadsTo (Acts prg)
-                         (reachable prg  Int  A)
-  		         (reachable prg  Int  B)"
+    "LeadsTo F A B ==
+		 leadsTo (Acts F)
+                         (reachable F  Int  A)
+  		         (reachable F  Int  B)"
 end