src/HOL/UNITY/WFair.thy
changeset 8006 299127ded09d
parent 7346 dace49c16aca
child 9685 6d123a7e30bd
--- a/src/HOL/UNITY/WFair.thy	Thu Nov 11 10:25:17 1999 +0100
+++ b/src/HOL/UNITY/WFair.thy	Thu Nov 11 10:25:29 1999 +0100
@@ -17,17 +17,15 @@
   transient :: "'a set => 'a program set"
     "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
 
+  ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
+    "A ensures B == (A-B co A Un B) Int transient (A-B)"
+
 
 consts
 
-  ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
-
   (*LEADS-TO constant for the inductive definition*)
   leads :: "'a program => ('a set * 'a set) set"
 
-  (*visible version of the LEADS-TO relation*)
-  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
-
 
 inductive "leads F"
   intrs 
@@ -44,13 +42,11 @@
   monos Pow_mono
 
 
-  
-defs
-  ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)"
+constdefs
 
-  leadsTo_def "A leadsTo B == {F. (A,B) : leads F}"
-
-constdefs
+  (*visible version of the LEADS-TO relation*)
+  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
+    "A leadsTo B == {F. (A,B) : leads F}"
   
   (*wlt F B is the largest set that leads to B*)
   wlt :: "['a program, 'a set] => 'a set"