--- a/src/CTT/Arith.ML Tue Oct 24 14:42:15 1995 +0100
+++ b/src/CTT/Arith.ML Tue Oct 24 14:45:35 1995 +0100
@@ -17,22 +17,22 @@
(*typing of add: short and long versions*)
-val add_typing = prove_goalw Arith.thy arith_defs
+qed_goalw "add_typing" Arith.thy arith_defs
"[| a:N; b:N |] ==> a #+ b : N"
(fn prems=> [ (typechk_tac prems) ]);
-val add_typingL = prove_goalw Arith.thy arith_defs
+qed_goalw "add_typingL" Arith.thy arith_defs
"[| a=c:N; b=d:N |] ==> a #+ b = c #+ d : N"
(fn prems=> [ (equal_tac prems) ]);
(*computation for add: 0 and successor cases*)
-val addC0 = prove_goalw Arith.thy arith_defs
+qed_goalw "addC0" Arith.thy arith_defs
"b:N ==> 0 #+ b = b : N"
(fn prems=> [ (rew_tac prems) ]);
-val addC_succ = prove_goalw Arith.thy arith_defs
+qed_goalw "addC_succ" Arith.thy arith_defs
"[| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
(fn prems=> [ (rew_tac prems) ]);
@@ -41,23 +41,23 @@
(*typing of mult: short and long versions*)
-val mult_typing = prove_goalw Arith.thy arith_defs
+qed_goalw "mult_typing" Arith.thy arith_defs
"[| a:N; b:N |] ==> a #* b : N"
(fn prems=>
[ (typechk_tac([add_typing]@prems)) ]);
-val mult_typingL = prove_goalw Arith.thy arith_defs
+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])) ]);
(*computation for mult: 0 and successor cases*)
-val multC0 = prove_goalw Arith.thy arith_defs
+qed_goalw "multC0" Arith.thy arith_defs
"b:N ==> 0 #* b = 0 : N"
(fn prems=> [ (rew_tac prems) ]);
-val multC_succ = prove_goalw Arith.thy arith_defs
+qed_goalw "multC_succ" Arith.thy arith_defs
"[| a:N; b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
(fn prems=> [ (rew_tac prems) ]);
@@ -66,11 +66,11 @@
(*typing of difference*)
-val diff_typing = prove_goalw Arith.thy arith_defs
+qed_goalw "diff_typing" Arith.thy arith_defs
"[| a:N; b:N |] ==> a - b : N"
(fn prems=> [ (typechk_tac prems) ]);
-val diff_typingL = prove_goalw Arith.thy arith_defs
+qed_goalw "diff_typingL" Arith.thy arith_defs
"[| a=c:N; b=d:N |] ==> a - b = c - d : N"
(fn prems=> [ (equal_tac prems) ]);
@@ -78,13 +78,13 @@
(*computation for difference: 0 and successor cases*)
-val diffC0 = prove_goalw Arith.thy arith_defs
+qed_goalw "diffC0" Arith.thy arith_defs
"a:N ==> a - 0 = a : N"
(fn prems=> [ (rew_tac prems) ]);
(*Note: rec(a, 0, %z w.z) is pred(a). *)
-val diff_0_eq_0 = prove_goalw Arith.thy arith_defs
+qed_goalw "diff_0_eq_0" Arith.thy arith_defs
"b:N ==> 0 - b = 0 : N"
(fn prems=>
[ (NE_tac "b" 1),
@@ -93,7 +93,7 @@
(*Essential to simplify FIRST!! (Else we get a critical pair)
succ(a) - succ(b) rewrites to pred(succ(a) - b) *)
-val diff_succ_succ = prove_goalw Arith.thy arith_defs
+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),
@@ -144,7 +144,7 @@
**********)
(*Associative law for addition*)
-val add_assoc = prove_goal Arith.thy
+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),
@@ -153,7 +153,7 @@
(*Commutative law for addition. Can be proved using three inductions.
Must simplify after first induction! Orientation of rewrites is delicate*)
-val add_commute = prove_goal Arith.thy
+qed_goal "add_commute" Arith.thy
"[| a:N; b:N |] ==> a #+ b = b #+ a : N"
(fn prems=>
[ (NE_tac "a" 1),
@@ -169,7 +169,7 @@
****************)
(*Commutative law for multiplication
-val mult_commute = prove_goal Arith.thy
+qed_goal "mult_commute" Arith.thy
"[| a:N; b:N |] ==> a #* b = b #* a : N"
(fn prems=>
[ (NE_tac "a" 1),
@@ -181,14 +181,14 @@
***************)
(*right annihilation in product*)
-val mult_0_right = prove_goal Arith.thy
+qed_goal "mult_0_right" Arith.thy
"a:N ==> a #* 0 = 0 : N"
(fn prems=>
[ (NE_tac "a" 1),
(hyp_arith_rew_tac prems) ]);
(*right successor law for multiplication*)
-val mult_succ_right = prove_goal Arith.thy
+qed_goal "mult_succ_right" Arith.thy
"[| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
(fn prems=>
[ (NE_tac "a" 1),
@@ -201,14 +201,14 @@
intrL_rls@[refl_elem]) 1)) ]);
(*Commutative law for multiplication*)
-val mult_commute = prove_goal Arith.thy
+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])) ]);
(*addition distributes over multiplication*)
-val add_mult_distrib = prove_goal Arith.thy
+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),
@@ -217,7 +217,7 @@
(*Associative law for multiplication*)
-val mult_assoc = prove_goal Arith.thy
+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),
@@ -231,7 +231,7 @@
Difference on natural numbers, without negative numbers
a - b = 0 iff a<=b a - b = succ(c) iff a>b *)
-val diff_self_eq_0 = prove_goal Arith.thy
+qed_goal "diff_self_eq_0" Arith.thy
"a:N ==> a - a = 0 : N"
(fn prems=>
[ (NE_tac "a" 1),
@@ -262,7 +262,7 @@
by (intr_tac[]); (*strips remaining PRODs*)
by (hyp_arith_rew_tac (prems@[add_0_right]));
by (assume_tac 1);
-val add_diff_inverse_lemma = result();
+qed "add_diff_inverse_lemma";
(*Version of above with premise b-a=0 i.e. a >= b.
@@ -274,7 +274,7 @@
by (resolve_tac [EqE] 1);
by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1);
by (REPEAT (resolve_tac (prems@[EqI]) 1));
-val add_diff_inverse = result();
+qed "add_diff_inverse";
(********************
@@ -283,26 +283,26 @@
(*typing of absolute difference: short and long versions*)
-val absdiff_typing = prove_goalw Arith.thy arith_defs
+qed_goalw "absdiff_typing" Arith.thy arith_defs
"[| a:N; b:N |] ==> a |-| b : N"
(fn prems=> [ (typechk_tac prems) ]);
-val absdiff_typingL = prove_goalw Arith.thy arith_defs
+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 absdiff_self_eq_0 = prove_goalw Arith.thy [absdiff_def]
+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])) ]);
-val absdiffC0 = prove_goalw Arith.thy [absdiff_def]
+qed_goalw "absdiffC0" Arith.thy [absdiff_def]
"a:N ==> 0 |-| a = a : N"
(fn prems=>
[ (hyp_arith_rew_tac prems) ]);
-val absdiff_succ_succ = prove_goalw Arith.thy [absdiff_def]
+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) ]);
@@ -312,7 +312,7 @@
"[| a:N; b:N |] ==> a |-| b = b |-| a : N";
by (resolve_tac [add_commute] 1);
by (typechk_tac ([diff_typing]@prems));
-val absdiff_commute = result();
+qed "absdiff_commute";
(*If a+b=0 then a=0. Surprisingly tedious*)
val prems =
@@ -324,7 +324,7 @@
by (resolve_tac [ zero_ne_succ RS FE ] 2);
by (etac (EqE RS sym_elem) 3);
by (typechk_tac ([add_typing] @prems));
-val add_eq0_lemma = result();
+qed "add_eq0_lemma";
(*Version of above with the premise a+b=0.
Again, resolution instantiates variables in ProdE *)
@@ -334,7 +334,7 @@
by (resolve_tac [add_eq0_lemma RS ProdE] 1);
by (resolve_tac [EqI] 3);
by (ALLGOALS (resolve_tac prems));
-val add_eq0 = result();
+qed "add_eq0";
(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
val prems = goalw Arith.thy [absdiff_def]
@@ -346,7 +346,7 @@
by (resolve_tac [add_eq0] 1);
by (resolve_tac [add_commute RS trans_elem] 6);
by (typechk_tac (diff_typing::prems));
-val absdiff_eq0_lem = result();
+qed "absdiff_eq0_lem";
(*if a |-| b = 0 then a = b
proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
@@ -359,7 +359,7 @@
by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1);
by (resolve_tac [EqE] 3 THEN assume_tac 3);
by (hyp_arith_rew_tac (prems@[add_0_right]));
-val absdiff_eq0 = result();
+qed "absdiff_eq0";
(***********************
Remainder and Quotient
@@ -367,12 +367,12 @@
(*typing of remainder: short and long versions*)
-val mod_typing = prove_goalw Arith.thy [mod_def]
+qed_goalw "mod_typing" Arith.thy [mod_def]
"[| a:N; b:N |] ==> a mod b : N"
(fn prems=>
[ (typechk_tac (absdiff_typing::prems)) ]);
-val mod_typingL = prove_goalw Arith.thy [mod_def]
+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])) ]);
@@ -380,11 +380,11 @@
(*computation for mod : 0 and successor cases*)
-val modC0 = prove_goalw Arith.thy [mod_def] "b:N ==> 0 mod b = 0 : N"
+qed_goalw "modC0" Arith.thy [mod_def] "b:N ==> 0 mod b = 0 : N"
(fn prems=>
[ (rew_tac(absdiff_typing::prems)) ]);
-val modC_succ = prove_goalw Arith.thy [mod_def]
+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)) ]);
@@ -392,11 +392,11 @@
(*typing of quotient: short and long versions*)
-val div_typing = prove_goalw Arith.thy [div_def] "[| a:N; b:N |] ==> a div b : N"
+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)) ]);
-val div_typingL = prove_goalw Arith.thy [div_def]
+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])) ]);
@@ -406,7 +406,7 @@
(*computation for quotient: 0 and successor cases*)
-val divC0 = prove_goalw Arith.thy [div_def] "b:N ==> 0 div b = 0 : N"
+qed_goalw "divC0" Arith.thy [div_def] "b:N ==> 0 div b = 0 : N"
(fn prems=>
[ (rew_tac([mod_typing, absdiff_typing] @ prems)) ]);
@@ -418,7 +418,7 @@
(*Version of above with same condition as the mod one*)
-val divC_succ2 = prove_goal Arith.thy
+qed_goal "divC_succ2" 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=>
@@ -428,7 +428,7 @@
(rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ]);
(*for case analysis on whether a number is 0 or a successor*)
-val iszero_decidable = prove_goal Arith.thy
+qed_goal "iszero_decidable" 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=>
@@ -455,6 +455,6 @@
by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);
by (resolve_tac [refl_elem] 3);
by (hyp_arith_rew_tac (prems @ div_typing_rls));
-val mod_div_equality = result();
+qed "mod_div_equality";
writeln"Reached end of file.";
--- a/src/CTT/Bool.ML Tue Oct 24 14:42:15 1995 +0100
+++ b/src/CTT/Bool.ML Tue Oct 24 14:45:35 1995 +0100
@@ -13,30 +13,30 @@
(*Derivation of rules for the type Bool*)
(*formation rule*)
-val boolF = prove_goalw Bool.thy bool_defs
+qed_goalw "boolF" Bool.thy bool_defs
"Bool type"
(fn _ => [ (typechk_tac []) ]);
(*introduction rules for true, false*)
-val boolI_true = prove_goalw Bool.thy bool_defs
+qed_goalw "boolI_true" Bool.thy bool_defs
"true : Bool"
(fn _ => [ (typechk_tac []) ]);
-val boolI_false = prove_goalw Bool.thy bool_defs
+qed_goalw "boolI_false" Bool.thy bool_defs
"false : Bool"
(fn _ => [ (typechk_tac []) ]);
(*elimination rule: typing of cond*)
-val boolE = prove_goalw Bool.thy bool_defs
+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 []) ]);
-val boolEL = prove_goalw Bool.thy bool_defs
+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 _ =>
@@ -45,7 +45,7 @@
(*computation rules for true, false*)
-val boolC_true = prove_goalw Bool.thy bool_defs
+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),
@@ -53,7 +53,7 @@
(ALLGOALS (etac TE)),
(typechk_tac []) ]);
-val boolC_false = prove_goalw Bool.thy bool_defs
+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),
--- a/src/CTT/CTT.ML Tue Oct 24 14:42:15 1995 +0100
+++ b/src/CTT/CTT.ML Tue Oct 24 14:45:35 1995 +0100
@@ -8,51 +8,6 @@
open CTT;
-signature CTT_RESOLVE =
- sig
- val add_mp_tac: int -> tactic
- val ASSUME: (int -> tactic) -> int -> tactic
- val basic_defs: thm list
- val comp_rls: thm list
- val element_rls: thm list
- val elimL_rls: thm list
- val elim_rls: thm list
- val eqintr_tac: tactic
- val equal_tac: thm list -> tactic
- val formL_rls: thm list
- val form_rls: thm list
- val form_tac: tactic
- val intrL2_rls: thm list
- val intrL_rls: thm list
- val intr_rls: thm list
- val intr_tac: thm list -> tactic
- val mp_tac: int -> tactic
- val NE_tac: string -> int -> tactic
- val pc_tac: thm list -> int -> tactic
- val PlusE_tac: string -> int -> tactic
- val reduction_rls: thm list
- val replace_type: thm
- val routine_rls: thm list
- val routine_tac: thm list -> thm list -> int -> tactic
- val safe_brls: (bool * thm) list
- val safestep_tac: thm list -> int -> tactic
- val safe_tac: thm list -> int -> tactic
- val step_tac: thm list -> int -> tactic
- val subst_eqtyparg: thm
- val subst_prodE: thm
- val SumE_fst: thm
- val SumE_snd: thm
- val SumE_tac: string -> int -> tactic
- val SumIL2: thm
- val test_assume_tac: int -> tactic
- val typechk_tac: thm list -> tactic
- val unsafe_brls: (bool * thm) list
- end;
-
-
-structure CTT_Resolve : CTT_RESOLVE =
-struct
-
(*Formation rules*)
val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
@@ -80,7 +35,7 @@
val basic_defs = [fst_def,snd_def];
(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
-val SumIL2 = prove_goal CTT.thy
+qed_goal "SumIL2" CTT.thy
"[| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
(fn prems=>
[ (resolve_tac [sym_elem] 1),
@@ -92,7 +47,7 @@
(*Exploit p:Prod(A,B) to create the assumption z:B(a).
A more natural form of product elimination. *)
-val subst_prodE = prove_goal CTT.thy
+qed_goal "subst_prodE" CTT.thy
"[| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z) \
\ |] ==> c(p`a): C(p`a)"
(fn prems=>
@@ -145,7 +100,7 @@
(*** Simplification ***)
(*To simplify the type in a goal*)
-val replace_type = prove_goal CTT.thy
+qed_goal "replace_type" CTT.thy
"[| B = A; a : A |] ==> a : B"
(fn prems=>
[ (resolve_tac [equal_types] 1),
@@ -153,7 +108,7 @@
(ALLGOALS (resolve_tac prems)) ]);
(*Simplify the parameter of a unary type operator.*)
-val subst_eqtyparg = prove_goal CTT.thy
+qed_goal "subst_eqtyparg" CTT.thy
"a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
(fn prems=>
[ (resolve_tac [subst_typeL] 1),
@@ -222,21 +177,17 @@
(** The elimination rules for fst/snd **)
-val SumE_fst = prove_goalw CTT.thy basic_defs
+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) ]);
(*The first premise must be p:Sum(A,B) !!*)
-val SumE_snd = prove_goalw CTT.thy basic_defs
+qed_goalw "SumE_snd" 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) ]);
-
-end;
-
-open CTT_Resolve;
--- a/src/CTT/Makefile Tue Oct 24 14:42:15 1995 +0100
+++ b/src/CTT/Makefile Tue Oct 24 14:45:35 1995 +0100
@@ -1,3 +1,4 @@
+# $Id$
#########################################################################
# #
# Makefile for Isabelle (CTT) #
@@ -5,9 +6,11 @@
#########################################################################
#To make the system, cd to this directory and type
-# make -f Makefile
+# make
#To make the system and test it on standard examples, type
-# make -f Makefile test
+# make test
+#To generate HTML files for every theory, set the environment variable
+#MAKE_HTML or add the parameter "MAKE_HTML=".
#Environment variable ISABELLECOMP specifies the compiler.
#Environment variable ISABELLEBIN specifies the destination directory.
@@ -32,8 +35,16 @@
case "$(COMP)" in \
poly*) echo 'make_database"$(BIN)/CTT"; quit();' \
| $(COMP) $(BIN)/Pure;\
- echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CTT ;;\
- sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/CTT" banner;' | $(BIN)/Pure ;;\
+ if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+ | $(COMP) $(BIN)/CTT;\
+ else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/CTT;\
+ fi;;\
+ sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+ then echo 'init_html (); exit_use"ROOT.ML"; xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
+ else echo 'exit_use"ROOT.ML"; xML"$(BIN)/CTT" banner;' \
+ | $(BIN)/Pure;\
+ fi;;\
*) echo Bad value for ISABELLECOMP: \
$(COMP) is not poly or sml;;\
esac
--- a/src/CTT/ROOT.ML Tue Oct 24 14:42:15 1995 +0100
+++ b/src/CTT/ROOT.ML Tue Oct 24 14:45:35 1995 +0100
@@ -23,4 +23,6 @@
use "../Pure/install_pp.ML";
print_depth 8;
+make_chart (); (*make HTML chart*)
+
val CTT_build_completed = (); (*indicate successful build*)
--- a/src/CTT/ex/ROOT.ML Tue Oct 24 14:42:15 1995 +0100
+++ b/src/CTT/ex/ROOT.ML Tue Oct 24 14:45:35 1995 +0100
@@ -17,4 +17,6 @@
time_use "ex/equal.ML";
time_use "ex/synth.ML";
+make_chart (); (*make HTML chart*)
+
maketest"END: Root file for CTT examples";
--- a/src/CTT/ex/equal.ML Tue Oct 24 14:42:15 1995 +0100
+++ b/src/CTT/ex/equal.ML Tue Oct 24 14:45:35 1995 +0100
@@ -11,7 +11,7 @@
by (rtac EqE 1);
by (resolve_tac elim_rls 1 THEN resolve_tac prems 1);
by (rew_tac prems);
-val split_eq = result();
+qed "split_eq";
val prems =
goal CTT.thy
@@ -19,7 +19,7 @@
by (rtac EqE 1);
by (resolve_tac elim_rls 1 THEN resolve_tac prems 1);
by (rew_tac prems);
-val when_eq = result();
+qed "when_eq";
(*in the "rec" formulation of addition, 0+n=n *)