# HG changeset patch
# User clasohm
# Date 785423481 -3600
# Node ID d9c629fbacc64ef647f4fa2f0a8031e5586d5106
# Parent  36c0ac2f49358319b6e15ab846b924dfeba5cc96
replaced 'val ... = result();' by 'qed "...";'

diff -r 36c0ac2f4935 -r d9c629fbacc6 src/FOL/ex/If.ML
--- a/src/FOL/ex/If.ML	Mon Nov 21 14:06:59 1994 +0100
+++ b/src/FOL/ex/If.ML	Mon Nov 21 14:11:21 1994 +0100
@@ -12,13 +12,13 @@
 val prems = goalw If.thy [if_def]
     "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
 by (fast_tac (FOL_cs addIs prems) 1);
-val ifI = result();
+qed "ifI";
 
 val major::prems = goalw If.thy [if_def]
    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
 by (cut_facts_tac [major] 1);
 by (fast_tac (FOL_cs addIs prems) 1);
-val ifE = result();
+qed "ifE";
 
 
 goal If.thy
diff -r 36c0ac2f4935 -r d9c629fbacc6 src/FOL/ex/List.ML
--- a/src/FOL/ex/List.ML	Mon Nov 21 14:06:59 1994 +0100
+++ b/src/FOL/ex/List.ML	Mon Nov 21 14:11:21 1994 +0100
@@ -11,7 +11,7 @@
 val prems = goal List.thy "[| P([]);  !!x l. P(x.l) |] ==> All(P)";
 by (rtac list_ind 1);
 by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
-val list_exh = result();
+qed "list_exh";
 
 val list_rew_thms = [list_distinct1,list_distinct2,app_nil,app_cons,
 		     hd_eq,tl_eq,forall_nil,forall_cons,list_free,
diff -r 36c0ac2f4935 -r d9c629fbacc6 src/FOL/ex/Nat2.ML
--- a/src/FOL/ex/Nat2.ML	Mon Nov 21 14:06:59 1994 +0100
+++ b/src/FOL/ex/Nat2.ML	Mon Nov 21 14:11:21 1994 +0100
@@ -20,7 +20,7 @@
     "[| P(0);  !!x. P(succ(x)) |] ==> All(P)";
 by (rtac nat_ind 1);
 by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
-val nat_exh = result();
+qed "nat_exh";
 
 goal Nat2.thy "~ n=succ(n)";
 by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
@@ -40,11 +40,11 @@
 
 goal Nat2.thy "m+0 = m";
 by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
-val plus_0_right = result();
+qed "plus_0_right";
 
 goal Nat2.thy "m+succ(n) = succ(m+n)";
 by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
-val plus_succ_right = result();
+qed "plus_succ_right";
 
 goal Nat2.thy "~n=0 --> m+pred(n) = pred(m+n)";
 by (IND_TAC nat_ind (simp_tac (nat_ss addsimps [plus_succ_right])) "n" 1);
@@ -64,6 +64,7 @@
 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);
 
 goal Nat2.thy "n<succ(n)";
 by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
@@ -95,7 +96,7 @@
 by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
 by (rtac (impI RS allI) 1);
 by (ALL_IND_TAC nat_ind (asm_simp_tac nat_ss) 1);
-val not_less = result();
+qed "not_less";
 
 goal Nat2.thy "n<=m --> ~m<n";
 by (simp_tac (nat_ss addsimps [not_less]) 1);