replaced "val ... = result()" by "qed ..."
--- a/src/FOL/ex/If.ML Tue Nov 29 11:51:07 1994 +0100
+++ b/src/FOL/ex/If.ML Wed Nov 30 13:13:52 1994 +0100
@@ -32,12 +32,12 @@
choplev 0;
val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];
by (fast_tac if_cs 1);
-val if_commute = result();
+qed "if_commute";
goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
by (fast_tac if_cs 1);
-val nested_ifs = result();
+qed "nested_ifs";
choplev 0;
by (rewrite_goals_tac [if_def]);
--- a/src/FOL/ex/List.ML Tue Nov 29 11:51:07 1994 +0100
+++ b/src/FOL/ex/List.ML Wed Nov 30 13:13:52 1994 +0100
@@ -25,43 +25,43 @@
goal List.thy "(l1++l2)++l3 = l1++(l2++l3)";
by(IND_TAC list_ind (simp_tac list_ss) "l1" 1);
-val append_assoc = result();
+qed "append_assoc";
goal List.thy "l++[] = l";
by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
-val app_nil_right = result();
+qed "app_nil_right";
goal List.thy "l1++l2=[] <-> l1=[] & l2=[]";
by(IND_TAC list_exh (simp_tac list_ss) "l1" 1);
-val app_eq_nil_iff = result();
+qed "app_eq_nil_iff";
goal List.thy "forall(l++l',P) <-> forall(l,P) & forall(l',P)";
by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
-val forall_app = result();
+qed "forall_app";
goal List.thy "forall(l,%x.P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
by(fast_tac FOL_cs 1);
-val forall_conj = result();
+qed "forall_conj";
goal List.thy "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)";
by(IND_TAC list_ind (simp_tac list_ss) "l" 1);
-val forall_ne = result();
+qed "forall_ne";
(*** Lists with natural numbers ***)
goal List.thy "len(l1++l2) = len(l1)+len(l2)";
by (IND_TAC list_ind (simp_tac list_ss) "l1" 1);
-val len_app = result();
+qed "len_app";
goal List.thy "i<len(l1) --> at(l1++l2,i) = at(l1,i)";
by (IND_TAC list_ind (simp_tac list_ss) "l1" 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
by (ALL_IND_TAC nat_exh (asm_simp_tac list_ss) 1);
-val at_app1 = result();
+qed "at_app1";
goal List.thy "at(l1++(x.l2), len(l1)) = x";
by (IND_TAC list_ind (simp_tac list_ss) "l1" 1);
-val at_app_hd2 = result();
+qed "at_app_hd2";
--- a/src/FOL/ex/Nat.ML Tue Nov 29 11:51:07 1994 +0100
+++ b/src/FOL/ex/Nat.ML Wed Nov 30 13:13:52 1994 +0100
@@ -22,7 +22,7 @@
by (resolve_tac [notI] 1);
by (eresolve_tac [notE] 1);
by (eresolve_tac [Suc_inject] 1);
-val Suc_n_not_n = result();
+qed "Suc_n_not_n";
goal Nat.thy "(k+m)+n = k+(m+n)";
@@ -37,11 +37,11 @@
goalw Nat.thy [add_def] "0+n = n";
by (resolve_tac [rec_0] 1);
-val add_0 = result();
+qed "add_0";
goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
by (resolve_tac [rec_Suc] 1);
-val add_Suc = result();
+qed "add_Suc";
val add_ss = FOL_ss addsimps [add_0, add_Suc];
@@ -49,18 +49,18 @@
by (res_inst_tac [("n","k")] induct 1);
by (simp_tac add_ss 1);
by (asm_simp_tac add_ss 1);
-val add_assoc = result();
+qed "add_assoc";
goal Nat.thy "m+0 = m";
by (res_inst_tac [("n","m")] induct 1);
by (simp_tac add_ss 1);
by (asm_simp_tac add_ss 1);
-val add_0_right = result();
+qed "add_0_right";
goal Nat.thy "m+Suc(n) = Suc(m+n)";
by (res_inst_tac [("n","m")] induct 1);
by (ALLGOALS (asm_simp_tac add_ss));
-val add_Suc_right = result();
+qed "add_Suc_right";
val [prem] = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
by (res_inst_tac [("n","i")] induct 1);
--- a/src/FOL/ex/Nat2.ML Tue Nov 29 11:51:07 1994 +0100
+++ b/src/FOL/ex/Nat2.ML Wed Nov 30 13:13:52 1994 +0100
@@ -63,8 +63,7 @@
by (rtac (impI RS allI) 1);
by (ALL_IND_TAC nat_ind (simp_tac nat_ss) 1);
by (fast_tac FOL_cs 1);
-val le_imp_le_succ = result() RS mp;
-store_thm("le_imp_le_succ", le_imp_le_succ);
+val le_imp_le_succ = store_thm("le_imp_le_succ", result() RS mp);
goal Nat2.thy "n<succ(n)";
by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
@@ -85,12 +84,12 @@
by (IND_TAC nat_ind
(simp_tac (nat_ss addsimps [plus_0_right, plus_succ_right, le_imp_le_succ]))
"k" 1);
-val le_plus = result();
+qed "le_plus";
goal Nat2.thy "succ(m) <= n --> m <= n";
by (res_inst_tac [("x","n")]spec 1);
by (ALL_IND_TAC nat_exh (simp_tac (nat_ss addsimps [le_imp_le_succ])) 1);
-val succ_le = result();
+qed "succ_le";
goal Nat2.thy "~m<n <-> n<=m";
by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
@@ -100,11 +99,11 @@
goal Nat2.thy "n<=m --> ~m<n";
by (simp_tac (nat_ss addsimps [not_less]) 1);
-val le_imp_not_less = result();
+qed "le_imp_not_less";
goal Nat2.thy "m<n --> ~n<=m";
by (cut_facts_tac [not_less] 1 THEN fast_tac FOL_cs 1);
-val not_le = result();
+qed "not_le";
goal Nat2.thy "m+k<=n --> m<=n";
by (IND_TAC nat_ind (K all_tac) "k" 1);
@@ -114,21 +113,21 @@
by (REPEAT (resolve_tac [allI,impI] 1));
by (cut_facts_tac [succ_le] 1);
by (fast_tac FOL_cs 1);
-val plus_le = result();
+qed "plus_le";
val prems = goal Nat2.thy "[| ~m=0; m <= n |] ==> ~n=0";
by (cut_facts_tac prems 1);
by (REPEAT (etac rev_mp 1));
by (IND_TAC nat_exh (simp_tac nat_ss) "m" 1);
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
-val not0 = result();
+qed "not0";
goal Nat2.thy "a<=a' & b<=b' --> a+b<=a'+b'";
by (IND_TAC nat_ind (simp_tac (nat_ss addsimps [plus_0_right,le_plus])) "b" 1);
by (resolve_tac [impI RS allI] 1);
by (resolve_tac [allI RS allI] 1);
by (ALL_IND_TAC nat_exh (asm_simp_tac (nat_ss addsimps [plus_succ_right])) 1);
-val plus_le_plus = result();
+qed "plus_le_plus";
goal Nat2.thy "i<=j --> j<=k --> i<=k";
by (IND_TAC nat_ind (K all_tac) "i" 1);
@@ -137,7 +136,7 @@
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
by (fast_tac FOL_cs 1);
-val le_trans = result();
+qed "le_trans";
goal Nat2.thy "i < j --> j <=k --> i < k";
by (IND_TAC nat_ind (K all_tac) "j" 1);
@@ -147,18 +146,18 @@
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
by (fast_tac FOL_cs 1);
-val less_le_trans = result();
+qed "less_le_trans";
goal Nat2.thy "succ(i) <= j <-> i < j";
by (IND_TAC nat_ind (simp_tac nat_ss) "j" 1);
by (resolve_tac [impI RS allI] 1);
by (ALL_IND_TAC nat_exh (asm_simp_tac nat_ss) 1);
-val succ_le = result();
+qed "succ_le2";
goal Nat2.thy "i<succ(j) <-> i=j | i<j";
by (IND_TAC nat_ind (simp_tac nat_ss) "j" 1);
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
by (resolve_tac [impI RS allI] 1);
by (ALL_IND_TAC nat_exh (asm_simp_tac nat_ss) 1);
-val less_succ = result();
+qed "less_succ";
--- a/src/FOL/ex/intro.ML Tue Nov 29 11:51:07 1994 +0100
+++ b/src/FOL/ex/intro.ML Wed Nov 30 13:13:52 1994 +0100
@@ -20,7 +20,7 @@
by (assume_tac 3);
by (assume_tac 2);
by (assume_tac 1);
-val mythm = result();
+qed "mythm";
goal FOL.thy "(P & Q) | R --> (P | R)";
by (resolve_tac [impI] 1);