src/HOL/UNITY/Token.thy
changeset 5253 82a5ca6290aa
parent 5232 e5a7cdd07ea5
child 5277 e4297d03e5d2
--- a/src/HOL/UNITY/Token.thy	Wed Aug 05 10:56:58 1998 +0200
+++ b/src/HOL/UNITY/Token.thy	Wed Aug 05 10:57:25 1998 +0200
@@ -44,18 +44,18 @@
 rules
   N_positive "0<N"
 
-  skip "id: Acts"
+  skip "id: acts"
 
-  TR2  "constrains Acts (T i) (T i Un H i)"
+  TR2  "constrains acts (T i) (T i Un H i)"
 
-  TR3  "constrains Acts (H i) (H i Un E i)"
+  TR3  "constrains acts (H i) (H i Un E i)"
 
-  TR4  "constrains Acts (H i - HasTok i) (H i)"
+  TR4  "constrains acts (H i - HasTok i) (H i)"
 
-  TR5  "constrains Acts (HasTok i) (HasTok i Un Compl(E i))"
+  TR5  "constrains acts (HasTok i) (HasTok i Un Compl(E i))"
 
-  TR6  "leadsTo Acts (H i Int HasTok i) (E i)"
+  TR6  "leadsTo acts (H i Int HasTok i) (E i)"
 
-  TR7  "leadsTo Acts (HasTok i) (HasTok (next i))"
+  TR7  "leadsTo acts (HasTok i) (HasTok (next i))"
 
 end