src/HOL/UNITY/Token.thy
changeset 5253 82a5ca6290aa
parent 5232 e5a7cdd07ea5
child 5277 e4297d03e5d2
     1.1 --- a/src/HOL/UNITY/Token.thy	Wed Aug 05 10:56:58 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Token.thy	Wed Aug 05 10:57:25 1998 +0200
     1.3 @@ -44,18 +44,18 @@
     1.4  rules
     1.5    N_positive "0<N"
     1.6  
     1.7 -  skip "id: Acts"
     1.8 +  skip "id: acts"
     1.9  
    1.10 -  TR2  "constrains Acts (T i) (T i Un H i)"
    1.11 +  TR2  "constrains acts (T i) (T i Un H i)"
    1.12  
    1.13 -  TR3  "constrains Acts (H i) (H i Un E i)"
    1.14 +  TR3  "constrains acts (H i) (H i Un E i)"
    1.15  
    1.16 -  TR4  "constrains Acts (H i - HasTok i) (H i)"
    1.17 +  TR4  "constrains acts (H i - HasTok i) (H i)"
    1.18  
    1.19 -  TR5  "constrains Acts (HasTok i) (HasTok i Un Compl(E i))"
    1.20 +  TR5  "constrains acts (HasTok i) (HasTok i Un Compl(E i))"
    1.21  
    1.22 -  TR6  "leadsTo Acts (H i Int HasTok i) (E i)"
    1.23 +  TR6  "leadsTo acts (H i Int HasTok i) (E i)"
    1.24  
    1.25 -  TR7  "leadsTo Acts (HasTok i) (HasTok (next i))"
    1.26 +  TR7  "leadsTo acts (HasTok i) (HasTok (next i))"
    1.27  
    1.28  end