# HG changeset patch # User clasohm # Date 786197632 -3600 # Node ID dfb3894d78e4fa1744b1e910412d129ce4d575fe # Parent 521a6f3ff27912fbff08c4955f3d33fbf076b1dd replaced "val ... = result()" by "qed ..." diff -r 521a6f3ff279 -r dfb3894d78e4 src/FOL/ex/If.ML --- 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]); diff -r 521a6f3ff279 -r dfb3894d78e4 src/FOL/ex/List.ML --- 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 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"; diff -r 521a6f3ff279 -r dfb3894d78e4 src/FOL/ex/Nat.ML --- 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); diff -r 521a6f3ff279 -r dfb3894d78e4 src/FOL/ex/Nat2.ML --- 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 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<=m"; by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1); @@ -100,11 +99,11 @@ goal Nat2.thy "n<=m --> ~m ~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 i=j | i (P | R)"; by (resolve_tac [impI] 1);