# HG changeset patch
# User paulson
# Date 962811726 -7200
# Node ID c71db8c2872796da54dfaf8dc1546721e6c9d89a
# Parent  e1dee89de0378f19d5e9a80528119c4b6de1d905
removed batch proofs

diff -r e1dee89de037 -r c71db8c28727 src/CTT/Arith.ML
--- a/src/CTT/Arith.ML	Wed Jul 05 16:37:52 2000 +0200
+++ b/src/CTT/Arith.ML	Wed Jul 05 17:42:06 2000 +0200
@@ -9,7 +9,6 @@
 Tests definitions and simplifier.
 *)
 
-open Arith;
 val arith_defs = [add_def, diff_def, absdiff_def, mult_def, mod_def, div_def];
 
 
@@ -17,88 +16,97 @@
 
 (*typing of add: short and long versions*)
 
-qed_goalw "add_typing" Arith.thy arith_defs
-    "[| a:N;  b:N |] ==> a #+ b : N"
- (fn prems=> [ (typechk_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "[| a:N;  b:N |] ==> a #+ b : N";
+by (typechk_tac prems) ;
+qed "add_typing";
 
-qed_goalw "add_typingL" Arith.thy arith_defs
-    "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N"
- (fn prems=> [ (equal_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N";
+by (equal_tac prems) ;
+qed "add_typingL";
 
 
 (*computation for add: 0 and successor cases*)
 
-qed_goalw "addC0" Arith.thy arith_defs
-    "b:N ==> 0 #+ b = b : N"
- (fn prems=> [ (rew_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "b:N ==> 0 #+ b = b : N";
+by (rew_tac prems) ;
+qed "addC0";
 
-qed_goalw "addC_succ" Arith.thy arith_defs
-    "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
- (fn prems=> [ (rew_tac prems) ]); 
+val prems= goalw Arith.thy arith_defs 
+    "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N";
+by (rew_tac prems) ;
+qed "addC_succ"; 
 
 
 (** Multiplication *)
 
 (*typing of mult: short and long versions*)
 
-qed_goalw "mult_typing" Arith.thy arith_defs
-    "[| a:N;  b:N |] ==> a #* b : N"
- (fn prems=>
-  [ (typechk_tac([add_typing]@prems)) ]);
+val prems= goalw Arith.thy arith_defs 
+    "[| a:N;  b:N |] ==> a #* b : N";
+by (typechk_tac([add_typing]@prems)) ;
+qed "mult_typing";
 
-qed_goalw "mult_typingL" Arith.thy arith_defs
-    "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
- (fn prems=>
-  [ (equal_tac (prems@[add_typingL])) ]);
+val prems= goalw Arith.thy arith_defs 
+    "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N";
+by (equal_tac (prems@[add_typingL])) ;
+qed "mult_typingL";
 
 (*computation for mult: 0 and successor cases*)
 
-qed_goalw "multC0" Arith.thy arith_defs
-    "b:N ==> 0 #* b = 0 : N"
- (fn prems=> [ (rew_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "b:N ==> 0 #* b = 0 : N";
+by (rew_tac prems) ;
+qed "multC0";
 
-qed_goalw "multC_succ" Arith.thy arith_defs
-    "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
- (fn prems=> [ (rew_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N";
+by (rew_tac prems) ;
+qed "multC_succ";
 
 
 (** Difference *)
 
 (*typing of difference*)
 
-qed_goalw "diff_typing" Arith.thy arith_defs
-    "[| a:N;  b:N |] ==> a - b : N"
- (fn prems=> [ (typechk_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "[| a:N;  b:N |] ==> a - b : N";
+by (typechk_tac prems) ;
+qed "diff_typing";
 
-qed_goalw "diff_typingL" Arith.thy arith_defs
-    "[| a=c:N;  b=d:N |] ==> a - b = c - d : N"
- (fn prems=> [ (equal_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "[| a=c:N;  b=d:N |] ==> a - b = c - d : N";
+by (equal_tac prems) ;
+qed "diff_typingL";
 
 
 
 (*computation for difference: 0 and successor cases*)
 
-qed_goalw "diffC0" Arith.thy arith_defs
-    "a:N ==> a - 0 = a : N"
- (fn prems=> [ (rew_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "a:N ==> a - 0 = a : N";
+by (rew_tac prems) ;
+qed "diffC0";
 
 (*Note: rec(a, 0, %z w.z) is pred(a). *)
 
-qed_goalw "diff_0_eq_0" Arith.thy arith_defs
-    "b:N ==> 0 - b = 0 : N"
- (fn prems=>
-  [ (NE_tac "b" 1),
-    (hyp_rew_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "b:N ==> 0 - b = 0 : N";
+by (NE_tac "b" 1);
+by (hyp_rew_tac prems) ;
+qed "diff_0_eq_0";
 
 
 (*Essential to simplify FIRST!!  (Else we get a critical pair)
   succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
-qed_goalw "diff_succ_succ" Arith.thy arith_defs
-    "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
- (fn prems=>
-  [ (hyp_rew_tac prems),
-    (NE_tac "b" 1),
-    (hyp_rew_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N";
+by (hyp_rew_tac prems);
+by (NE_tac "b" 1);
+by (hyp_rew_tac prems) ;
+qed "diff_succ_succ";
 
 
 
@@ -144,24 +152,24 @@
  **********)
 
 (*Associative law for addition*)
-qed_goal "add_assoc" Arith.thy 
-    "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
- (fn prems=>
-  [ (NE_tac "a" 1),
-    (hyp_arith_rew_tac prems) ]);
+val prems= goal Arith.thy 
+    "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N";
+by (NE_tac "a" 1);
+by (hyp_arith_rew_tac prems) ;
+qed "add_assoc";
 
 
 (*Commutative law for addition.  Can be proved using three inductions.
   Must simplify after first induction!  Orientation of rewrites is delicate*)  
-qed_goal "add_commute" Arith.thy 
-    "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
- (fn prems=>
-  [ (NE_tac "a" 1),
-    (hyp_arith_rew_tac prems),
-    (NE_tac "b" 2),
-    (rtac sym_elem 1),
-    (NE_tac "b" 1),
-    (hyp_arith_rew_tac prems) ]);
+val prems= goal Arith.thy 
+    "[| a:N;  b:N |] ==> a #+ b = b #+ a : N";
+by (NE_tac "a" 1);
+by (hyp_arith_rew_tac prems);
+by (NE_tac "b" 2);
+by (rtac sym_elem 1);
+by (NE_tac "b" 1);
+by (hyp_arith_rew_tac prems) ;
+qed "add_commute";
 
 
 (****************
@@ -169,59 +177,53 @@
  ****************)
 
 (*Commutative law for multiplication
-qed_goal "mult_commute" Arith.thy 
-    "[| a:N;  b:N |] ==> a #* b = b #* a : N"
- (fn prems=>
-  [ (NE_tac "a" 1),
-    (hyp_arith_rew_tac prems),
-    (NE_tac "b" 2),
-    (rtac sym_elem 1),
-    (NE_tac "b" 1),
-    (hyp_arith_rew_tac prems) ]);   NEEDS COMMUTATIVE MATCHING
+val prems= goal Arith.thy 
+    "[| a:N;  b:N |] ==> a #* b = b #* a : N";
+by (NE_tac "a" 1);
+by (hyp_arith_rew_tac prems);
+by (NE_tac "b" 2);
+by (rtac sym_elem 1);
+by (NE_tac "b" 1);
+by (hyp_arith_rew_tac prems) ;
+qed "mult_commute";   NEEDS COMMUTATIVE MATCHING
 ***************)
 
 (*right annihilation in product*)
-qed_goal "mult_0_right" Arith.thy 
-    "a:N ==> a #* 0 = 0 : N"
- (fn prems=>
-  [ (NE_tac "a" 1),
-    (hyp_arith_rew_tac prems) ]);
+val prems= goal Arith.thy 
+    "a:N ==> a #* 0 = 0 : N";
+by (NE_tac "a" 1);
+by (hyp_arith_rew_tac prems) ;
+qed "mult_0_right";
 
 (*right successor law for multiplication*)
-qed_goal "mult_succ_right" Arith.thy 
-    "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
- (fn prems=>
-  [ (NE_tac "a" 1),
-(*swap round the associative law of addition*)
-    (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])),  
-(*leaves a goal involving a commutative law*)
-    (REPEAT (assume_tac 1  ORELSE  
-            resolve_tac
-             (prems@[add_commute,mult_typingL,add_typingL]@
-               intrL_rls@[refl_elem])   1)) ]);
+val prems= goal Arith.thy 
+    "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N";
+by (NE_tac "a" 1);
+by (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem]));
+by (REPEAT (assume_tac 1  ORELSE resolve_tac (prems@[add_commute,mult_typingL,add_typingL]@ intrL_rls@[refl_elem])   1)) ;
+qed "mult_succ_right";
 
 (*Commutative law for multiplication*)
-qed_goal "mult_commute" Arith.thy 
-    "[| a:N;  b:N |] ==> a #* b = b #* a : N"
- (fn prems=>
-  [ (NE_tac "a" 1),
-    (hyp_arith_rew_tac (prems @ [mult_0_right, mult_succ_right])) ]);
+val prems= goal Arith.thy 
+    "[| a:N;  b:N |] ==> a #* b = b #* a : N";
+by (NE_tac "a" 1);
+by (hyp_arith_rew_tac (prems @ [mult_0_right, mult_succ_right])) ;
+qed "mult_commute";
 
 (*addition distributes over multiplication*)
-qed_goal "add_mult_distrib" Arith.thy 
-    "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
- (fn prems=>
-  [ (NE_tac "a" 1),
-(*swap round the associative law of addition*)
-    (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])) ]);
+val prems= goal Arith.thy 
+    "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N";
+by (NE_tac "a" 1);
+by (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])) ;
+qed "add_mult_distrib";
 
 
 (*Associative law for multiplication*)
-qed_goal "mult_assoc" Arith.thy 
-    "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
- (fn prems=>
-  [ (NE_tac "a" 1),
-    (hyp_arith_rew_tac (prems @ [add_mult_distrib])) ]);
+val prems= goal Arith.thy 
+    "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N";
+by (NE_tac "a" 1);
+by (hyp_arith_rew_tac (prems @ [add_mult_distrib])) ;
+qed "mult_assoc";
 
 
 (************
@@ -231,11 +233,11 @@
 Difference on natural numbers, without negative numbers
   a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *)
 
-qed_goal "diff_self_eq_0" Arith.thy 
-    "a:N ==> a - a = 0 : N"
- (fn prems=>
-  [ (NE_tac "a" 1),
-    (hyp_arith_rew_tac prems) ]);
+val prems= goal Arith.thy 
+    "a:N ==> a - a = 0 : N";
+by (NE_tac "a" 1);
+by (hyp_arith_rew_tac prems) ;
+qed "diff_self_eq_0";
 
 
 (*  [| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N  *)
@@ -283,29 +285,31 @@
 
 (*typing of absolute difference: short and long versions*)
 
-qed_goalw "absdiff_typing" Arith.thy arith_defs
-    "[| a:N;  b:N |] ==> a |-| b : N"
- (fn prems=> [ (typechk_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "[| a:N;  b:N |] ==> a |-| b : N";
+by (typechk_tac prems) ;
+qed "absdiff_typing";
 
-qed_goalw "absdiff_typingL" Arith.thy arith_defs
-    "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N"
- (fn prems=> [ (equal_tac prems) ]);
+val prems= goalw Arith.thy arith_defs 
+    "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N";
+by (equal_tac prems) ;
+qed "absdiff_typingL";
 
-qed_goalw "absdiff_self_eq_0" Arith.thy [absdiff_def]
-    "a:N ==> a |-| a = 0 : N"
- (fn prems=>
-  [ (arith_rew_tac (prems@[diff_self_eq_0])) ]);
+Goalw [absdiff_def]  
+    "a:N ==> a |-| a = 0 : N";
+by (arith_rew_tac (prems@[diff_self_eq_0])) ;
+qed "absdiff_self_eq_0";
 
-qed_goalw "absdiffC0" Arith.thy [absdiff_def]
-    "a:N ==> 0 |-| a = a : N"
- (fn prems=>
-  [ (hyp_arith_rew_tac prems) ]);
+Goalw [absdiff_def]  
+    "a:N ==> 0 |-| a = a : N";
+by (hyp_arith_rew_tac []);
+qed "absdiffC0";
 
 
-qed_goalw "absdiff_succ_succ" Arith.thy [absdiff_def]
-    "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N"
- (fn prems=>
-  [ (hyp_arith_rew_tac prems) ]);
+Goalw [absdiff_def]  
+    "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N";
+by (hyp_arith_rew_tac []) ;
+qed "absdiff_succ_succ";
 
 (*Note how easy using commutative laws can be?  ...not always... *)
 val prems = goalw Arith.thy [absdiff_def]
@@ -367,76 +371,78 @@
 
 (*typing of remainder: short and long versions*)
 
-qed_goalw "mod_typing" Arith.thy [mod_def]
-    "[| a:N;  b:N |] ==> a mod b : N"
- (fn prems=>
-  [ (typechk_tac (absdiff_typing::prems)) ]);
+Goalw [mod_def]  
+    "[| a:N;  b:N |] ==> a mod b : N";
+by (typechk_tac (absdiff_typing::prems)) ;
+qed "mod_typing";
  
-qed_goalw "mod_typingL" Arith.thy [mod_def]
-    "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
- (fn prems=>
-  [ (equal_tac (prems@[absdiff_typingL])) ]);
+Goalw [mod_def]  
+    "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N";
+by (equal_tac [absdiff_typingL]) ;
+by (ALLGOALS assume_tac);
+qed "mod_typingL";
  
 
 (*computation for  mod : 0 and successor cases*)
 
-qed_goalw "modC0" Arith.thy [mod_def] "b:N ==> 0 mod b = 0 : N"
- (fn prems=>
-  [ (rew_tac(absdiff_typing::prems)) ]);
+Goalw [mod_def]   "b:N ==> 0 mod b = 0 : N";
+by (rew_tac(absdiff_typing::prems)) ;
+qed "modC0";
 
-qed_goalw "modC_succ" Arith.thy [mod_def] 
-"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
- (fn prems=>
-  [ (rew_tac(absdiff_typing::prems)) ]);
+Goalw [mod_def]   
+"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N";
+by (rew_tac(absdiff_typing::prems)) ;
+qed "modC_succ";
 
 
 (*typing of quotient: short and long versions*)
 
-qed_goalw "div_typing" Arith.thy [div_def] "[| a:N;  b:N |] ==> a div b : N"
- (fn prems=>
-  [ (typechk_tac ([absdiff_typing,mod_typing]@prems)) ]);
+Goalw [div_def]   "[| a:N;  b:N |] ==> a div b : N";
+by (typechk_tac ([absdiff_typing,mod_typing]@prems)) ;
+qed "div_typing";
 
-qed_goalw "div_typingL" Arith.thy [div_def]
-   "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
- (fn prems=>
-  [ (equal_tac (prems @ [absdiff_typingL, mod_typingL])) ]);
+Goalw [div_def]  
+   "[| a=c:N;  b=d:N |] ==> a div b = c div d : N";
+by (equal_tac [absdiff_typingL, mod_typingL]);
+by (ALLGOALS assume_tac);
+qed "div_typingL";
 
 val div_typing_rls = [mod_typing, div_typing, absdiff_typing];
 
 
 (*computation for quotient: 0 and successor cases*)
 
-qed_goalw "divC0" Arith.thy [div_def] "b:N ==> 0 div b = 0 : N"
- (fn prems=>
-  [ (rew_tac([mod_typing, absdiff_typing] @ prems)) ]);
+Goalw [div_def]   "b:N ==> 0 div b = 0 : N";
+by (rew_tac([mod_typing, absdiff_typing] @ prems)) ;
+qed "divC0";
 
-val divC_succ =
-prove_goalw Arith.thy [div_def] "[| a:N;  b:N |] ==> succ(a) div b = \
-\    rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
- (fn prems=>
-  [ (rew_tac([mod_typing]@prems)) ]);
+Goalw [div_def] 
+ "[| a:N;  b:N |] ==> succ(a) div b = \
+\    rec(succ(a) mod b, succ(a div b), %x y. a div b) : N";
+by (rew_tac([mod_typing]@prems)) ;
+qed "divC_succ";
 
 
 (*Version of above with same condition as the  mod  one*)
-qed_goal "divC_succ2" Arith.thy
+val prems= goal Arith.thy
     "[| a:N;  b:N |] ==> \
-\    succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
- (fn prems=>
-  [ (resolve_tac [ divC_succ RS trans_elem ] 1),
-    (rew_tac(div_typing_rls @ prems @ [modC_succ])),
-    (NE_tac "succ(a mod b)|-|b" 1),
-    (rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ]);
+\    succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N";
+by (resolve_tac [ divC_succ RS trans_elem ] 1);
+by (rew_tac(div_typing_rls @ prems @ [modC_succ]));
+by (NE_tac "succ(a mod b)|-|b" 1);
+by (rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ;
+qed "divC_succ2";
 
 (*for case analysis on whether a number is 0 or a successor*)
-qed_goal "iszero_decidable" Arith.thy
+val prems= goal Arith.thy
     "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \
-\                     Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
- (fn prems=>
-  [ (NE_tac "a" 1),
-    (rtac PlusI_inr 3),
-    (rtac PlusI_inl 2),
-    eqintr_tac,
-    (equal_tac prems) ]);
+\                     Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))";
+by (NE_tac "a" 1);
+by (rtac PlusI_inr 3);
+by (rtac PlusI_inl 2);
+by eqintr_tac;
+by (equal_tac prems) ;
+qed "iszero_decidable";
 
 (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
 val prems =
diff -r e1dee89de037 -r c71db8c28727 src/CTT/Bool.ML
--- a/src/CTT/Bool.ML	Wed Jul 05 16:37:52 2000 +0200
+++ b/src/CTT/Bool.ML	Wed Jul 05 17:42:06 2000 +0200
@@ -6,60 +6,58 @@
 Theorems for bool.thy (booleans and conditionals)
 *)
 
-open Bool;
-
 val bool_defs = [Bool_def,true_def,false_def,cond_def];
 
 (*Derivation of rules for the type Bool*)
 
 (*formation rule*)
-qed_goalw "boolF" Bool.thy bool_defs 
-    "Bool type"
- (fn _ => [ (typechk_tac []) ]);
+Goalw bool_defs "Bool type";
+by (typechk_tac []) ;
+qed "boolF";
 
 
 (*introduction rules for true, false*)
 
-qed_goalw "boolI_true" Bool.thy bool_defs 
-    "true : Bool"
- (fn _ => [ (typechk_tac []) ]);
+Goalw bool_defs "true : Bool";
+by (typechk_tac []) ;
+qed "boolI_true";
 
-qed_goalw "boolI_false" Bool.thy bool_defs 
-    "false : Bool"
- (fn _ => [ (typechk_tac []) ]);
+Goalw bool_defs "false : Bool";
+by (typechk_tac []) ;
+qed "boolI_false";
 
 (*elimination rule: typing of cond*)
-qed_goalw "boolE" 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 []) ]);
+Goalw bool_defs 
+    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)";
+by (typechk_tac []);
+by (ALLGOALS (etac TE));
+by (typechk_tac []) ;
+qed "boolE";
 
-qed_goalw "boolEL" 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 _ =>
-  [ (rtac PlusEL 1),
-    (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ]);
+Goalw bool_defs
+    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |] \
+\    ==> cond(p,a,b) = cond(q,c,d) : C(p)";
+by (rtac PlusEL 1);
+by (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ;
+qed "boolEL";
 
 (*computation rules for true, false*)
 
-qed_goalw "boolC_true" 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 []) ]);
+Goalw bool_defs 
+    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)";
+by (resolve_tac comp_rls 1);
+by (typechk_tac []);
+by (ALLGOALS (etac TE));
+by (typechk_tac []) ;
+qed "boolC_true";
 
-qed_goalw "boolC_false" 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 []) ]);
+Goalw bool_defs
+    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)";
+by (resolve_tac comp_rls 1);
+by (typechk_tac []);
+by (ALLGOALS (etac TE));
+by (typechk_tac []) ;
+qed "boolC_false";
 
 writeln"Reached end of file.";
 
diff -r e1dee89de037 -r c71db8c28727 src/CTT/CTT.ML
--- a/src/CTT/CTT.ML	Wed Jul 05 16:37:52 2000 +0200
+++ b/src/CTT/CTT.ML	Wed Jul 05 17:42:06 2000 +0200
@@ -6,8 +6,6 @@
 Tactics and lemmas for ctt.thy (Constructive Type Theory)
 *)
 
-open CTT;
-
 (*Formation rules*)
 val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
 and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
@@ -35,23 +33,23 @@
 val basic_defs = [fst_def,snd_def];
 
 (*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
-qed_goal "SumIL2" CTT.thy
-    "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
- (fn prems=>
-  [ (rtac sym_elem 1),
-    (rtac SumIL 1),
-    (ALLGOALS (rtac sym_elem )),
-    (ALLGOALS (resolve_tac prems)) ]);
+val prems= goal CTT.thy
+    "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)";
+by (rtac sym_elem 1);
+by (rtac SumIL 1);
+by (ALLGOALS (rtac sym_elem ));
+by (ALLGOALS (resolve_tac prems)) ;
+qed "SumIL2";
 
 val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
 
 (*Exploit p:Prod(A,B) to create the assumption z:B(a).  
   A more natural form of product elimination. *)
-qed_goal "subst_prodE" CTT.thy
+val prems= goal CTT.thy
     "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
-\    |] ==> c(p`a): C(p`a)"
- (fn prems=>
-  [ (REPEAT (resolve_tac (prems@[ProdE]) 1)) ]);
+\    |] ==> c(p`a): C(p`a)";
+by (REPEAT (resolve_tac (prems@[ProdE]) 1)) ;
+qed "subst_prodE";
 
 (** Tactics for type checking **)
 
@@ -100,21 +98,21 @@
 (*** Simplification ***)
 
 (*To simplify the type in a goal*)
-qed_goal "replace_type" CTT.thy
-    "[| B = A;  a : A |] ==> a : B"
- (fn prems=>
-  [ (rtac equal_types 1),
-    (rtac sym_type 2),
-    (ALLGOALS (resolve_tac prems)) ]);
+val prems= goal CTT.thy
+    "[| B = A;  a : A |] ==> a : B";
+by (rtac equal_types 1);
+by (rtac sym_type 2);
+by (ALLGOALS (resolve_tac prems)) ;
+qed "replace_type";
 
 (*Simplify the parameter of a unary type operator.*)
-qed_goal "subst_eqtyparg" CTT.thy
-    "a=c : A ==> (!!z. z:A ==> B(z) type) ==> B(a)=B(c)"
- (fn prems=>
-  [ (rtac subst_typeL 1),
-    (rtac refl_type 2),
-    (ALLGOALS (resolve_tac prems)),
-    (assume_tac 1) ]);
+val prems= goal CTT.thy
+    "a=c : A ==> (!!z. z:A ==> B(z) type) ==> B(a)=B(c)";
+by (rtac subst_typeL 1);
+by (rtac refl_type 2);
+by (ALLGOALS (resolve_tac prems));
+by (assume_tac 1) ;
+qed "subst_eqtyparg";
 
 (*Make a reduction rule for simplification.
   A goal a=c becomes b=c, by virtue of a=b *)
@@ -177,17 +175,17 @@
 
 (** The elimination rules for fst/snd **)
 
-qed_goalw "SumE_fst" CTT.thy basic_defs
-    "p : Sum(A,B) ==> fst(p) : A"
- (fn [major] =>
-  [ (rtac (major RS SumE) 1),
-    (assume_tac 1) ]);
+val [major] = goalw CTT.thy basic_defs
+    "p : Sum(A,B) ==> fst(p) : A";
+by (rtac (major RS SumE) 1);
+by (assume_tac 1) ;
+qed "SumE_fst";
 
 (*The first premise must be p:Sum(A,B) !!*)
-qed_goalw "SumE_snd" CTT.thy basic_defs
+val major::prems= goalw CTT.thy basic_defs
     "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
-\    |] ==> snd(p) : B(fst(p))"
- (fn major::prems=>
-  [ (rtac (major RS SumE) 1),
-    (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1),
-    (typechk_tac prems) ]);
+\    |] ==> snd(p) : B(fst(p))";
+by (rtac (major RS SumE) 1);
+by (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1);
+by (typechk_tac prems) ;
+qed "SumE_snd";