1.1 --- a/src/HOL/UNITY/WFair.thy	Thu Nov 11 10:25:17 1999 +0100
     1.2 +++ b/src/HOL/UNITY/WFair.thy	Thu Nov 11 10:25:29 1999 +0100
     1.3 @@ -17,17 +17,15 @@
     1.4    transient :: "'a set => 'a program set"
     1.5      "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
     1.6  
     1.7 +  ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
     1.8 +    "A ensures B == (A-B co A Un B) Int transient (A-B)"
     1.9 +
    1.10  
    1.11  consts
    1.12  
    1.13 -  ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
    1.14 -
    1.15    (*LEADS-TO constant for the inductive definition*)
    1.16    leads :: "'a program => ('a set * 'a set) set"
    1.17  
    1.18 -  (*visible version of the LEADS-TO relation*)
    1.19 -  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
    1.20 -
    1.21  
    1.22  inductive "leads F"
    1.23    intrs 
    1.24 @@ -44,13 +42,11 @@
    1.25    monos Pow_mono
    1.26  
    1.27  
    1.28 -  
    1.29 -defs
    1.30 -  ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)"
    1.31 +constdefs
    1.32  
    1.33 -  leadsTo_def "A leadsTo B == {F. (A,B) : leads F}"
    1.34 -
    1.35 -constdefs
    1.36 +  (*visible version of the LEADS-TO relation*)
    1.37 +  leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
    1.38 +    "A leadsTo B == {F. (A,B) : leads F}"
    1.39    
    1.40    (*wlt F B is the largest set that leads to B*)
    1.41    wlt :: "['a program, 'a set] => 'a set"