--- a/src/HOL/Hoare/Examples.ML Mon Mar 09 16:16:21 1998 +0100
+++ b/src/HOL/Hoare/Examples.ML Mon Mar 09 16:17:28 1998 +0100
@@ -59,7 +59,7 @@
\ b:=b div 2 \
\ END; \
\ c:=c*a; \
-\ b:=pred b \
+\ b:= b - 1 \
\ END \
\ {c = A^B}";
--- a/src/HOL/ex/Fib.ML Mon Mar 09 16:16:21 1998 +0100
+++ b/src/HOL/ex/Fib.ML Mon Mar 09 16:17:28 1998 +0100
@@ -49,7 +49,7 @@
(*Concrete Mathematics, page 278: Cassini's identity*)
goal thy "fib (Suc (Suc n)) * fib n = \
-\ (if n mod 2 = 0 then pred(fib(Suc n) * fib(Suc n)) \
+\ (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n)) - 1 \
\ else Suc (fib(Suc n) * fib(Suc n)))";
by (res_inst_tac [("u","n")] fib.induct 1);
by (res_inst_tac [("P", "%z. ?ff(x) * z = ?kk(x)")] (fib_Suc_Suc RS ssubst) 3);
--- a/src/HOLCF/IOA/NTP/Multiset.ML Mon Mar 09 16:16:21 1998 +0100
+++ b/src/HOLCF/IOA/NTP/Multiset.ML Mon Mar 09 16:17:28 1998 +0100
@@ -25,7 +25,7 @@
qed "count_leq_addm";
goalw Multiset.thy [Multiset.count_def]
- "count (delm M x) y = (if y=x then pred(count M y) else count M y)";
+ "count (delm M x) y = (if y=x then count M y - 1 else count M y)";
by (res_inst_tac [("M","M")] Multiset.induction 1);
by (asm_simp_tac (simpset()
addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]
@@ -67,7 +67,7 @@
qed_spec_mp "pos_count_imp_pos_countm";
goal Multiset.thy
- "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = pred (countm M P)";
+ "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1";
by (res_inst_tac [("M","M")] Multiset.induction 1);
by (simp_tac (simpset() addsimps
[Multiset.delm_empty_def,