added calls of init_html and make_chart;
authorclasohm
Tue Oct 24 14:45:35 1995 +0100 (1995-10-24)
changeset 12941358dc040edb
parent 1293 4ade5d1d369c
child 1295 27c1e88a62b4
added calls of init_html and make_chart;
added usage of qed
src/CTT/Arith.ML
src/CTT/Bool.ML
src/CTT/CTT.ML
src/CTT/Makefile
src/CTT/ROOT.ML
src/CTT/ex/ROOT.ML
src/CTT/ex/equal.ML
     1.1 --- a/src/CTT/Arith.ML	Tue Oct 24 14:42:15 1995 +0100
     1.2 +++ b/src/CTT/Arith.ML	Tue Oct 24 14:45:35 1995 +0100
     1.3 @@ -17,22 +17,22 @@
     1.4  
     1.5  (*typing of add: short and long versions*)
     1.6  
     1.7 -val add_typing = prove_goalw Arith.thy arith_defs
     1.8 +qed_goalw "add_typing" Arith.thy arith_defs
     1.9      "[| a:N;  b:N |] ==> a #+ b : N"
    1.10   (fn prems=> [ (typechk_tac prems) ]);
    1.11  
    1.12 -val add_typingL = prove_goalw Arith.thy arith_defs
    1.13 +qed_goalw "add_typingL" Arith.thy arith_defs
    1.14      "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N"
    1.15   (fn prems=> [ (equal_tac prems) ]);
    1.16  
    1.17  
    1.18  (*computation for add: 0 and successor cases*)
    1.19  
    1.20 -val addC0 = prove_goalw Arith.thy arith_defs
    1.21 +qed_goalw "addC0" Arith.thy arith_defs
    1.22      "b:N ==> 0 #+ b = b : N"
    1.23   (fn prems=> [ (rew_tac prems) ]);
    1.24  
    1.25 -val addC_succ = prove_goalw Arith.thy arith_defs
    1.26 +qed_goalw "addC_succ" Arith.thy arith_defs
    1.27      "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
    1.28   (fn prems=> [ (rew_tac prems) ]); 
    1.29  
    1.30 @@ -41,23 +41,23 @@
    1.31  
    1.32  (*typing of mult: short and long versions*)
    1.33  
    1.34 -val mult_typing = prove_goalw Arith.thy arith_defs
    1.35 +qed_goalw "mult_typing" Arith.thy arith_defs
    1.36      "[| a:N;  b:N |] ==> a #* b : N"
    1.37   (fn prems=>
    1.38    [ (typechk_tac([add_typing]@prems)) ]);
    1.39  
    1.40 -val mult_typingL = prove_goalw Arith.thy arith_defs
    1.41 +qed_goalw "mult_typingL" Arith.thy arith_defs
    1.42      "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
    1.43   (fn prems=>
    1.44    [ (equal_tac (prems@[add_typingL])) ]);
    1.45  
    1.46  (*computation for mult: 0 and successor cases*)
    1.47  
    1.48 -val multC0 = prove_goalw Arith.thy arith_defs
    1.49 +qed_goalw "multC0" Arith.thy arith_defs
    1.50      "b:N ==> 0 #* b = 0 : N"
    1.51   (fn prems=> [ (rew_tac prems) ]);
    1.52  
    1.53 -val multC_succ = prove_goalw Arith.thy arith_defs
    1.54 +qed_goalw "multC_succ" Arith.thy arith_defs
    1.55      "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
    1.56   (fn prems=> [ (rew_tac prems) ]);
    1.57  
    1.58 @@ -66,11 +66,11 @@
    1.59  
    1.60  (*typing of difference*)
    1.61  
    1.62 -val diff_typing = prove_goalw Arith.thy arith_defs
    1.63 +qed_goalw "diff_typing" Arith.thy arith_defs
    1.64      "[| a:N;  b:N |] ==> a - b : N"
    1.65   (fn prems=> [ (typechk_tac prems) ]);
    1.66  
    1.67 -val diff_typingL = prove_goalw Arith.thy arith_defs
    1.68 +qed_goalw "diff_typingL" Arith.thy arith_defs
    1.69      "[| a=c:N;  b=d:N |] ==> a - b = c - d : N"
    1.70   (fn prems=> [ (equal_tac prems) ]);
    1.71  
    1.72 @@ -78,13 +78,13 @@
    1.73  
    1.74  (*computation for difference: 0 and successor cases*)
    1.75  
    1.76 -val diffC0 = prove_goalw Arith.thy arith_defs
    1.77 +qed_goalw "diffC0" Arith.thy arith_defs
    1.78      "a:N ==> a - 0 = a : N"
    1.79   (fn prems=> [ (rew_tac prems) ]);
    1.80  
    1.81  (*Note: rec(a, 0, %z w.z) is pred(a). *)
    1.82  
    1.83 -val diff_0_eq_0 = prove_goalw Arith.thy arith_defs
    1.84 +qed_goalw "diff_0_eq_0" Arith.thy arith_defs
    1.85      "b:N ==> 0 - b = 0 : N"
    1.86   (fn prems=>
    1.87    [ (NE_tac "b" 1),
    1.88 @@ -93,7 +93,7 @@
    1.89  
    1.90  (*Essential to simplify FIRST!!  (Else we get a critical pair)
    1.91    succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
    1.92 -val diff_succ_succ = prove_goalw Arith.thy arith_defs
    1.93 +qed_goalw "diff_succ_succ" Arith.thy arith_defs
    1.94      "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
    1.95   (fn prems=>
    1.96    [ (hyp_rew_tac prems),
    1.97 @@ -144,7 +144,7 @@
    1.98   **********)
    1.99  
   1.100  (*Associative law for addition*)
   1.101 -val add_assoc = prove_goal Arith.thy 
   1.102 +qed_goal "add_assoc" Arith.thy 
   1.103      "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
   1.104   (fn prems=>
   1.105    [ (NE_tac "a" 1),
   1.106 @@ -153,7 +153,7 @@
   1.107  
   1.108  (*Commutative law for addition.  Can be proved using three inductions.
   1.109    Must simplify after first induction!  Orientation of rewrites is delicate*)  
   1.110 -val add_commute = prove_goal Arith.thy 
   1.111 +qed_goal "add_commute" Arith.thy 
   1.112      "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
   1.113   (fn prems=>
   1.114    [ (NE_tac "a" 1),
   1.115 @@ -169,7 +169,7 @@
   1.116   ****************)
   1.117  
   1.118  (*Commutative law for multiplication
   1.119 -val mult_commute = prove_goal Arith.thy 
   1.120 +qed_goal "mult_commute" Arith.thy 
   1.121      "[| a:N;  b:N |] ==> a #* b = b #* a : N"
   1.122   (fn prems=>
   1.123    [ (NE_tac "a" 1),
   1.124 @@ -181,14 +181,14 @@
   1.125  ***************)
   1.126  
   1.127  (*right annihilation in product*)
   1.128 -val mult_0_right = prove_goal Arith.thy 
   1.129 +qed_goal "mult_0_right" Arith.thy 
   1.130      "a:N ==> a #* 0 = 0 : N"
   1.131   (fn prems=>
   1.132    [ (NE_tac "a" 1),
   1.133      (hyp_arith_rew_tac prems) ]);
   1.134  
   1.135  (*right successor law for multiplication*)
   1.136 -val mult_succ_right = prove_goal Arith.thy 
   1.137 +qed_goal "mult_succ_right" Arith.thy 
   1.138      "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
   1.139   (fn prems=>
   1.140    [ (NE_tac "a" 1),
   1.141 @@ -201,14 +201,14 @@
   1.142  	       intrL_rls@[refl_elem])   1)) ]);
   1.143  
   1.144  (*Commutative law for multiplication*)
   1.145 -val mult_commute = prove_goal Arith.thy 
   1.146 +qed_goal "mult_commute" Arith.thy 
   1.147      "[| a:N;  b:N |] ==> a #* b = b #* a : N"
   1.148   (fn prems=>
   1.149    [ (NE_tac "a" 1),
   1.150      (hyp_arith_rew_tac (prems @ [mult_0_right, mult_succ_right])) ]);
   1.151  
   1.152  (*addition distributes over multiplication*)
   1.153 -val add_mult_distrib = prove_goal Arith.thy 
   1.154 +qed_goal "add_mult_distrib" Arith.thy 
   1.155      "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
   1.156   (fn prems=>
   1.157    [ (NE_tac "a" 1),
   1.158 @@ -217,7 +217,7 @@
   1.159  
   1.160  
   1.161  (*Associative law for multiplication*)
   1.162 -val mult_assoc = prove_goal Arith.thy 
   1.163 +qed_goal "mult_assoc" Arith.thy 
   1.164      "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
   1.165   (fn prems=>
   1.166    [ (NE_tac "a" 1),
   1.167 @@ -231,7 +231,7 @@
   1.168  Difference on natural numbers, without negative numbers
   1.169    a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *)
   1.170  
   1.171 -val diff_self_eq_0 = prove_goal Arith.thy 
   1.172 +qed_goal "diff_self_eq_0" Arith.thy 
   1.173      "a:N ==> a - a = 0 : N"
   1.174   (fn prems=>
   1.175    [ (NE_tac "a" 1),
   1.176 @@ -262,7 +262,7 @@
   1.177  by (intr_tac[]);  (*strips remaining PRODs*)
   1.178  by (hyp_arith_rew_tac (prems@[add_0_right]));  
   1.179  by (assume_tac 1);
   1.180 -val add_diff_inverse_lemma = result();
   1.181 +qed "add_diff_inverse_lemma";
   1.182  
   1.183  
   1.184  (*Version of above with premise   b-a=0   i.e.    a >= b.
   1.185 @@ -274,7 +274,7 @@
   1.186  by (resolve_tac [EqE] 1);
   1.187  by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1);
   1.188  by (REPEAT (resolve_tac (prems@[EqI]) 1));
   1.189 -val add_diff_inverse = result();
   1.190 +qed "add_diff_inverse";
   1.191  
   1.192  
   1.193  (********************
   1.194 @@ -283,26 +283,26 @@
   1.195  
   1.196  (*typing of absolute difference: short and long versions*)
   1.197  
   1.198 -val absdiff_typing = prove_goalw Arith.thy arith_defs
   1.199 +qed_goalw "absdiff_typing" Arith.thy arith_defs
   1.200      "[| a:N;  b:N |] ==> a |-| b : N"
   1.201   (fn prems=> [ (typechk_tac prems) ]);
   1.202  
   1.203 -val absdiff_typingL = prove_goalw Arith.thy arith_defs
   1.204 +qed_goalw "absdiff_typingL" Arith.thy arith_defs
   1.205      "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N"
   1.206   (fn prems=> [ (equal_tac prems) ]);
   1.207  
   1.208 -val absdiff_self_eq_0 = prove_goalw Arith.thy [absdiff_def]
   1.209 +qed_goalw "absdiff_self_eq_0" Arith.thy [absdiff_def]
   1.210      "a:N ==> a |-| a = 0 : N"
   1.211   (fn prems=>
   1.212    [ (arith_rew_tac (prems@[diff_self_eq_0])) ]);
   1.213  
   1.214 -val absdiffC0 = prove_goalw Arith.thy [absdiff_def]
   1.215 +qed_goalw "absdiffC0" Arith.thy [absdiff_def]
   1.216      "a:N ==> 0 |-| a = a : N"
   1.217   (fn prems=>
   1.218    [ (hyp_arith_rew_tac prems) ]);
   1.219  
   1.220  
   1.221 -val absdiff_succ_succ = prove_goalw Arith.thy [absdiff_def]
   1.222 +qed_goalw "absdiff_succ_succ" Arith.thy [absdiff_def]
   1.223      "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N"
   1.224   (fn prems=>
   1.225    [ (hyp_arith_rew_tac prems) ]);
   1.226 @@ -312,7 +312,7 @@
   1.227      "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
   1.228  by (resolve_tac [add_commute] 1);
   1.229  by (typechk_tac ([diff_typing]@prems));
   1.230 -val absdiff_commute = result();
   1.231 +qed "absdiff_commute";
   1.232  
   1.233  (*If a+b=0 then a=0.   Surprisingly tedious*)
   1.234  val prems =
   1.235 @@ -324,7 +324,7 @@
   1.236  by (resolve_tac [ zero_ne_succ RS FE ] 2);
   1.237  by (etac (EqE RS sym_elem) 3);
   1.238  by (typechk_tac ([add_typing] @prems));
   1.239 -val add_eq0_lemma = result();
   1.240 +qed "add_eq0_lemma";
   1.241  
   1.242  (*Version of above with the premise  a+b=0.
   1.243    Again, resolution instantiates variables in ProdE *)
   1.244 @@ -334,7 +334,7 @@
   1.245  by (resolve_tac [add_eq0_lemma RS ProdE] 1);
   1.246  by (resolve_tac [EqI] 3);
   1.247  by (ALLGOALS (resolve_tac prems));
   1.248 -val add_eq0 = result();
   1.249 +qed "add_eq0";
   1.250  
   1.251  (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
   1.252  val prems = goalw Arith.thy [absdiff_def]
   1.253 @@ -346,7 +346,7 @@
   1.254  by (resolve_tac [add_eq0] 1);
   1.255  by (resolve_tac [add_commute RS trans_elem] 6);
   1.256  by (typechk_tac (diff_typing::prems));
   1.257 -val absdiff_eq0_lem = result();
   1.258 +qed "absdiff_eq0_lem";
   1.259  
   1.260  (*if  a |-| b = 0  then  a = b  
   1.261    proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
   1.262 @@ -359,7 +359,7 @@
   1.263  by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1);
   1.264  by (resolve_tac [EqE] 3  THEN  assume_tac 3);
   1.265  by (hyp_arith_rew_tac (prems@[add_0_right]));
   1.266 -val absdiff_eq0 = result();
   1.267 +qed "absdiff_eq0";
   1.268  
   1.269  (***********************
   1.270    Remainder and Quotient
   1.271 @@ -367,12 +367,12 @@
   1.272  
   1.273  (*typing of remainder: short and long versions*)
   1.274  
   1.275 -val mod_typing = prove_goalw Arith.thy [mod_def]
   1.276 +qed_goalw "mod_typing" Arith.thy [mod_def]
   1.277      "[| a:N;  b:N |] ==> a mod b : N"
   1.278   (fn prems=>
   1.279    [ (typechk_tac (absdiff_typing::prems)) ]);
   1.280   
   1.281 -val mod_typingL = prove_goalw Arith.thy [mod_def]
   1.282 +qed_goalw "mod_typingL" Arith.thy [mod_def]
   1.283      "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
   1.284   (fn prems=>
   1.285    [ (equal_tac (prems@[absdiff_typingL])) ]);
   1.286 @@ -380,11 +380,11 @@
   1.287  
   1.288  (*computation for  mod : 0 and successor cases*)
   1.289  
   1.290 -val modC0 = prove_goalw Arith.thy [mod_def] "b:N ==> 0 mod b = 0 : N"
   1.291 +qed_goalw "modC0" Arith.thy [mod_def] "b:N ==> 0 mod b = 0 : N"
   1.292   (fn prems=>
   1.293    [ (rew_tac(absdiff_typing::prems)) ]);
   1.294  
   1.295 -val modC_succ = prove_goalw Arith.thy [mod_def] 
   1.296 +qed_goalw "modC_succ" Arith.thy [mod_def] 
   1.297  "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y.succ(a mod b)) : N"
   1.298   (fn prems=>
   1.299    [ (rew_tac(absdiff_typing::prems)) ]);
   1.300 @@ -392,11 +392,11 @@
   1.301  
   1.302  (*typing of quotient: short and long versions*)
   1.303  
   1.304 -val div_typing = prove_goalw Arith.thy [div_def] "[| a:N;  b:N |] ==> a div b : N"
   1.305 +qed_goalw "div_typing" Arith.thy [div_def] "[| a:N;  b:N |] ==> a div b : N"
   1.306   (fn prems=>
   1.307    [ (typechk_tac ([absdiff_typing,mod_typing]@prems)) ]);
   1.308  
   1.309 -val div_typingL = prove_goalw Arith.thy [div_def]
   1.310 +qed_goalw "div_typingL" Arith.thy [div_def]
   1.311     "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
   1.312   (fn prems=>
   1.313    [ (equal_tac (prems @ [absdiff_typingL, mod_typingL])) ]);
   1.314 @@ -406,7 +406,7 @@
   1.315  
   1.316  (*computation for quotient: 0 and successor cases*)
   1.317  
   1.318 -val divC0 = prove_goalw Arith.thy [div_def] "b:N ==> 0 div b = 0 : N"
   1.319 +qed_goalw "divC0" Arith.thy [div_def] "b:N ==> 0 div b = 0 : N"
   1.320   (fn prems=>
   1.321    [ (rew_tac([mod_typing, absdiff_typing] @ prems)) ]);
   1.322  
   1.323 @@ -418,7 +418,7 @@
   1.324  
   1.325  
   1.326  (*Version of above with same condition as the  mod  one*)
   1.327 -val divC_succ2 = prove_goal Arith.thy
   1.328 +qed_goal "divC_succ2" Arith.thy
   1.329      "[| a:N;  b:N |] ==> \
   1.330  \    succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
   1.331   (fn prems=>
   1.332 @@ -428,7 +428,7 @@
   1.333      (rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ]);
   1.334  
   1.335  (*for case analysis on whether a number is 0 or a successor*)
   1.336 -val iszero_decidable = prove_goal Arith.thy
   1.337 +qed_goal "iszero_decidable" Arith.thy
   1.338      "a:N ==> rec(a, inl(eq), %ka kb.inr(<ka, eq>)) : \
   1.339  \		      Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
   1.340   (fn prems=>
   1.341 @@ -455,6 +455,6 @@
   1.342  by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);
   1.343  by (resolve_tac [refl_elem] 3);
   1.344  by (hyp_arith_rew_tac (prems @ div_typing_rls)); 
   1.345 -val mod_div_equality = result();
   1.346 +qed "mod_div_equality";
   1.347  
   1.348  writeln"Reached end of file.";
     2.1 --- a/src/CTT/Bool.ML	Tue Oct 24 14:42:15 1995 +0100
     2.2 +++ b/src/CTT/Bool.ML	Tue Oct 24 14:45:35 1995 +0100
     2.3 @@ -13,30 +13,30 @@
     2.4  (*Derivation of rules for the type Bool*)
     2.5  
     2.6  (*formation rule*)
     2.7 -val boolF = prove_goalw Bool.thy bool_defs 
     2.8 +qed_goalw "boolF" Bool.thy bool_defs 
     2.9      "Bool type"
    2.10   (fn _ => [ (typechk_tac []) ]);
    2.11  
    2.12  
    2.13  (*introduction rules for true, false*)
    2.14  
    2.15 -val boolI_true = prove_goalw Bool.thy bool_defs 
    2.16 +qed_goalw "boolI_true" Bool.thy bool_defs 
    2.17      "true : Bool"
    2.18   (fn _ => [ (typechk_tac []) ]);
    2.19  
    2.20 -val boolI_false = prove_goalw Bool.thy bool_defs 
    2.21 +qed_goalw "boolI_false" Bool.thy bool_defs 
    2.22      "false : Bool"
    2.23   (fn _ => [ (typechk_tac []) ]);
    2.24  
    2.25  (*elimination rule: typing of cond*)
    2.26 -val boolE = prove_goalw Bool.thy bool_defs 
    2.27 +qed_goalw "boolE" Bool.thy bool_defs 
    2.28      "!!C. [| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
    2.29   (fn _ =>
    2.30    [ (typechk_tac []),
    2.31      (ALLGOALS (etac TE)),
    2.32      (typechk_tac []) ]);
    2.33  
    2.34 -val boolEL = prove_goalw Bool.thy bool_defs 
    2.35 +qed_goalw "boolEL" Bool.thy bool_defs 
    2.36      "!!C. [| p = q : Bool;  a = c : C(true);  b = d : C(false) |] ==> \
    2.37  \         cond(p,a,b) = cond(q,c,d) : C(p)"
    2.38   (fn _ =>
    2.39 @@ -45,7 +45,7 @@
    2.40  
    2.41  (*computation rules for true, false*)
    2.42  
    2.43 -val boolC_true = prove_goalw Bool.thy bool_defs 
    2.44 +qed_goalw "boolC_true" Bool.thy bool_defs 
    2.45      "!!C. [| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
    2.46   (fn _ =>
    2.47    [ (resolve_tac comp_rls 1),
    2.48 @@ -53,7 +53,7 @@
    2.49      (ALLGOALS (etac TE)),
    2.50      (typechk_tac []) ]);
    2.51  
    2.52 -val boolC_false = prove_goalw Bool.thy bool_defs 
    2.53 +qed_goalw "boolC_false" Bool.thy bool_defs 
    2.54      "!!C. [| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
    2.55   (fn _ =>
    2.56    [ (resolve_tac comp_rls 1),
     3.1 --- a/src/CTT/CTT.ML	Tue Oct 24 14:42:15 1995 +0100
     3.2 +++ b/src/CTT/CTT.ML	Tue Oct 24 14:45:35 1995 +0100
     3.3 @@ -8,51 +8,6 @@
     3.4  
     3.5  open CTT;
     3.6  
     3.7 -signature CTT_RESOLVE = 
     3.8 -  sig
     3.9 -  val add_mp_tac: int -> tactic
    3.10 -  val ASSUME: (int -> tactic) -> int -> tactic
    3.11 -  val basic_defs: thm list
    3.12 -  val comp_rls: thm list
    3.13 -  val element_rls: thm list
    3.14 -  val elimL_rls: thm list
    3.15 -  val elim_rls: thm list
    3.16 -  val eqintr_tac: tactic
    3.17 -  val equal_tac: thm list -> tactic
    3.18 -  val formL_rls: thm list
    3.19 -  val form_rls: thm list
    3.20 -  val form_tac: tactic
    3.21 -  val intrL2_rls: thm list
    3.22 -  val intrL_rls: thm list
    3.23 -  val intr_rls: thm list
    3.24 -  val intr_tac: thm list -> tactic
    3.25 -  val mp_tac: int -> tactic
    3.26 -  val NE_tac: string -> int -> tactic
    3.27 -  val pc_tac: thm list -> int -> tactic
    3.28 -  val PlusE_tac: string -> int -> tactic
    3.29 -  val reduction_rls: thm list
    3.30 -  val replace_type: thm
    3.31 -  val routine_rls: thm list   
    3.32 -  val routine_tac: thm list -> thm list -> int -> tactic
    3.33 -  val safe_brls: (bool * thm) list
    3.34 -  val safestep_tac: thm list -> int -> tactic
    3.35 -  val safe_tac: thm list -> int -> tactic
    3.36 -  val step_tac: thm list -> int -> tactic
    3.37 -  val subst_eqtyparg: thm
    3.38 -  val subst_prodE: thm
    3.39 -  val SumE_fst: thm
    3.40 -  val SumE_snd: thm
    3.41 -  val SumE_tac: string -> int -> tactic
    3.42 -  val SumIL2: thm
    3.43 -  val test_assume_tac: int -> tactic
    3.44 -  val typechk_tac: thm list -> tactic
    3.45 -  val unsafe_brls: (bool * thm) list
    3.46 -  end;
    3.47 -
    3.48 -
    3.49 -structure CTT_Resolve : CTT_RESOLVE = 
    3.50 -struct
    3.51 -
    3.52  (*Formation rules*)
    3.53  val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
    3.54  and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
    3.55 @@ -80,7 +35,7 @@
    3.56  val basic_defs = [fst_def,snd_def];
    3.57  
    3.58  (*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
    3.59 -val SumIL2 = prove_goal CTT.thy
    3.60 +qed_goal "SumIL2" CTT.thy
    3.61      "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
    3.62   (fn prems=>
    3.63    [ (resolve_tac [sym_elem] 1),
    3.64 @@ -92,7 +47,7 @@
    3.65  
    3.66  (*Exploit p:Prod(A,B) to create the assumption z:B(a).  
    3.67    A more natural form of product elimination. *)
    3.68 -val subst_prodE = prove_goal CTT.thy
    3.69 +qed_goal "subst_prodE" CTT.thy
    3.70      "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
    3.71  \    |] ==> c(p`a): C(p`a)"
    3.72   (fn prems=>
    3.73 @@ -145,7 +100,7 @@
    3.74  (*** Simplification ***)
    3.75  
    3.76  (*To simplify the type in a goal*)
    3.77 -val replace_type = prove_goal CTT.thy
    3.78 +qed_goal "replace_type" CTT.thy
    3.79      "[| B = A;  a : A |] ==> a : B"
    3.80   (fn prems=>
    3.81    [ (resolve_tac [equal_types] 1),
    3.82 @@ -153,7 +108,7 @@
    3.83      (ALLGOALS (resolve_tac prems)) ]);
    3.84  
    3.85  (*Simplify the parameter of a unary type operator.*)
    3.86 -val subst_eqtyparg = prove_goal CTT.thy
    3.87 +qed_goal "subst_eqtyparg" CTT.thy
    3.88      "a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
    3.89   (fn prems=>
    3.90    [ (resolve_tac [subst_typeL] 1),
    3.91 @@ -222,21 +177,17 @@
    3.92  
    3.93  (** The elimination rules for fst/snd **)
    3.94  
    3.95 -val SumE_fst = prove_goalw CTT.thy basic_defs
    3.96 +qed_goalw "SumE_fst" CTT.thy basic_defs
    3.97      "p : Sum(A,B) ==> fst(p) : A"
    3.98   (fn [major] =>
    3.99    [ (rtac (major RS SumE) 1),
   3.100      (assume_tac 1) ]);
   3.101  
   3.102  (*The first premise must be p:Sum(A,B) !!*)
   3.103 -val SumE_snd = prove_goalw CTT.thy basic_defs
   3.104 +qed_goalw "SumE_snd" CTT.thy basic_defs
   3.105      "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
   3.106  \    |] ==> snd(p) : B(fst(p))"
   3.107   (fn major::prems=>
   3.108    [ (rtac (major RS SumE) 1),
   3.109      (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1),
   3.110      (typechk_tac prems) ]);
   3.111 -
   3.112 -end;
   3.113 -
   3.114 -open CTT_Resolve;
     4.1 --- a/src/CTT/Makefile	Tue Oct 24 14:42:15 1995 +0100
     4.2 +++ b/src/CTT/Makefile	Tue Oct 24 14:45:35 1995 +0100
     4.3 @@ -1,3 +1,4 @@
     4.4 +# $Id$
     4.5  #########################################################################
     4.6  #									#
     4.7  # 			Makefile for Isabelle (CTT)			#
     4.8 @@ -5,9 +6,11 @@
     4.9  #########################################################################
    4.10  
    4.11  #To make the system, cd to this directory and type  
    4.12 -#	make -f Makefile 
    4.13 +#	make
    4.14  #To make the system and test it on standard examples, type  
    4.15 -#	make -f Makefile test
    4.16 +#	make test
    4.17 +#To generate HTML files for every theory, set the environment variable
    4.18 +#MAKE_HTML or add the parameter "MAKE_HTML=".
    4.19  
    4.20  #Environment variable ISABELLECOMP specifies the compiler.
    4.21  #Environment variable ISABELLEBIN specifies the destination directory.
    4.22 @@ -32,8 +35,16 @@
    4.23  	case "$(COMP)" in \
    4.24  	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
    4.25  			| $(COMP) $(BIN)/Pure;\
    4.26 -		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CTT ;;\
    4.27 -	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/CTT" banner;' | $(BIN)/Pure ;;\
    4.28 +                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    4.29 +                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
    4.30 +                       | $(COMP) $(BIN)/CTT;\
    4.31 +		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CTT;\
    4.32 +                fi;;\
    4.33 +	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    4.34 +                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
    4.35 +                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/CTT" banner;' \
    4.36 +                       | $(BIN)/Pure;\
    4.37 +                fi;;\
    4.38  	*)	echo Bad value for ISABELLECOMP: \
    4.39                  	$(COMP) is not poly or sml;;\
    4.40  	esac
     5.1 --- a/src/CTT/ROOT.ML	Tue Oct 24 14:42:15 1995 +0100
     5.2 +++ b/src/CTT/ROOT.ML	Tue Oct 24 14:45:35 1995 +0100
     5.3 @@ -23,4 +23,6 @@
     5.4  use "../Pure/install_pp.ML";
     5.5  print_depth 8;
     5.6  
     5.7 +make_chart ();   (*make HTML chart*)
     5.8 +
     5.9  val CTT_build_completed = ();	(*indicate successful build*)
     6.1 --- a/src/CTT/ex/ROOT.ML	Tue Oct 24 14:42:15 1995 +0100
     6.2 +++ b/src/CTT/ex/ROOT.ML	Tue Oct 24 14:45:35 1995 +0100
     6.3 @@ -17,4 +17,6 @@
     6.4  time_use "ex/equal.ML";
     6.5  time_use "ex/synth.ML";
     6.6  
     6.7 +make_chart ();   (*make HTML chart*)
     6.8 +
     6.9  maketest"END: Root file for CTT examples";
     7.1 --- a/src/CTT/ex/equal.ML	Tue Oct 24 14:42:15 1995 +0100
     7.2 +++ b/src/CTT/ex/equal.ML	Tue Oct 24 14:45:35 1995 +0100
     7.3 @@ -11,7 +11,7 @@
     7.4  by (rtac EqE 1);
     7.5  by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
     7.6  by (rew_tac prems);
     7.7 -val split_eq = result();
     7.8 +qed "split_eq";
     7.9  
    7.10  val prems =
    7.11  goal CTT.thy
    7.12 @@ -19,7 +19,7 @@
    7.13  by (rtac EqE 1);
    7.14  by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
    7.15  by (rew_tac prems);
    7.16 -val when_eq = result();
    7.17 +qed "when_eq";
    7.18  
    7.19  
    7.20  (*in the "rec" formulation of addition, 0+n=n *)