# HG changeset patch
# User wenzelm
# Date 889456648 -3600
# Node ID 05e57f1879ee432b2b487a9245cb57a93dbac104
# Parent  d24168720303650e29a9daf47365115049571477
eliminated pred function;

diff -r d24168720303 -r 05e57f1879ee src/HOL/Hoare/Examples.ML
--- 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}";
 
diff -r d24168720303 -r 05e57f1879ee src/HOL/ex/Fib.ML
--- 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);
diff -r d24168720303 -r 05e57f1879ee src/HOLCF/IOA/NTP/Multiset.ML
--- 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,