# HG changeset patch
# User lcp
# Date 768066450 -7200
# Node ID 2b74eebdbdb81da660139084f0916e9e9674b6e1
# Parent  b5a2e9503a7ab2777310fe4309fee5de00607f05
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw

diff -r b5a2e9503a7a -r 2b74eebdbdb8 src/CTT/Bool.ML
--- a/src/CTT/Bool.ML	Tue May 03 18:38:28 1994 +0200
+++ b/src/CTT/Bool.ML	Wed May 04 17:47:30 1994 +0200
@@ -13,67 +13,53 @@
 (*Derivation of rules for the type Bool*)
 
 (*formation rule*)
-val boolF = prove_goal Bool.thy 
+val boolF = prove_goalw Bool.thy bool_defs 
     "Bool type"
- (fn prems=>
-  [ (rewrite_goals_tac bool_defs),
-    (typechk_tac[]) ]);
+ (fn _ => [ (typechk_tac []) ]);
 
 
 (*introduction rules for true, false*)
 
-val boolI_true = prove_goal Bool.thy 
+val boolI_true = prove_goalw Bool.thy bool_defs 
     "true : Bool"
- (fn prems=>
-  [ (rewrite_goals_tac bool_defs),
-    (typechk_tac[]) ]);
+ (fn _ => [ (typechk_tac []) ]);
 
-val boolI_false = prove_goal Bool.thy 
+val boolI_false = prove_goalw Bool.thy bool_defs 
     "false : Bool"
- (fn prems=>
-  [ (rewrite_goals_tac bool_defs),
-    (typechk_tac[]) ]);
+ (fn _ => [ (typechk_tac []) ]);
 
 (*elimination rule: typing of cond*)
-val boolE = prove_goal Bool.thy 
-    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
- (fn prems=>
-  [ (cut_facts_tac prems 1),
-    (rewrite_goals_tac bool_defs),
-    (typechk_tac prems),
+val boolE = prove_goalw Bool.thy bool_defs 
+    "!!C. [| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
+ (fn _ =>
+  [ (typechk_tac []),
     (ALLGOALS (etac TE)),
-    (typechk_tac prems) ]);
+    (typechk_tac []) ]);
 
-val boolEL = prove_goal Bool.thy 
-    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |] ==> \
-\    cond(p,a,b) = cond(q,c,d) : C(p)"
- (fn prems=>
-  [ (cut_facts_tac prems 1),
-    (rewrite_goals_tac bool_defs),
-    (resolve_tac [PlusEL] 1),
+val boolEL = prove_goalw Bool.thy bool_defs 
+    "!!C. [| p = q : Bool;  a = c : C(true);  b = d : C(false) |] ==> \
+\         cond(p,a,b) = cond(q,c,d) : C(p)"
+ (fn _ =>
+  [ (resolve_tac [PlusEL] 1),
     (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ]);
 
 (*computation rules for true, false*)
 
-val boolC_true = prove_goal Bool.thy 
-    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
- (fn prems=>
-  [ (cut_facts_tac prems 1),
-    (rewrite_goals_tac bool_defs),
-    (resolve_tac comp_rls 1),
-    (typechk_tac[]),
+val boolC_true = prove_goalw Bool.thy bool_defs 
+    "!!C. [| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
+ (fn _ =>
+  [ (resolve_tac comp_rls 1),
+    (typechk_tac []),
     (ALLGOALS (etac TE)),
-    (typechk_tac prems) ]);
+    (typechk_tac []) ]);
 
-val boolC_false = prove_goal Bool.thy 
-    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
- (fn prems=>
-  [ (cut_facts_tac prems 1),
-    (rewrite_goals_tac bool_defs),
-    (resolve_tac comp_rls 1),
-    (typechk_tac[]),
+val boolC_false = prove_goalw Bool.thy bool_defs 
+    "!!C. [| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
+ (fn _ =>
+  [ (resolve_tac comp_rls 1),
+    (typechk_tac []),
     (ALLGOALS (etac TE)),
-    (typechk_tac prems) ]);
+    (typechk_tac []) ]);
 
 writeln"Reached end of file.";