--- a/src/HOL/UNITY/Comp/Counterc.thy Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.thy Fri Oct 05 21:52:39 2001 +0200
@@ -24,20 +24,20 @@
sumj :: "[nat, nat, state]=>int"
primrec (* sum I s = sigma_{i<I}. c s i *)
- "sum 0 s = #0"
+ "sum 0 s = Numeral0"
"sum (Suc i) s = (c s) i + sum i s"
primrec
- "sumj 0 i s = #0"
+ "sumj 0 i s = Numeral0"
"sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
types command = "(state*state)set"
constdefs
a :: "nat=>command"
- "a i == {(s, s'). (c s') i = (c s) i + #1 & (C s') = (C s) + #1}"
+ "a i == {(s, s'). (c s') i = (c s) i + Numeral1 & (C s') = (C s) + Numeral1}"
Component :: "nat => state program"
- "Component i == mk_program({s. C s = #0 & (c s) i = #0}, {a i},
+ "Component i == mk_program({s. C s = Numeral0 & (c s) i = Numeral0}, {a i},
UN G: preserves (%s. (c s) i). Acts G)"
end