Introduced qed_spec_mp.

--- a/src/HOL/IMP/Equiv.ML	Fri Feb 09 13:41:18 1996 +0100
+++ b/src/HOL/IMP/Equiv.ML	Fri Feb 09 13:41:59 1996 +0100
@@ -9,21 +9,21 @@
 by (ALLGOALS Simp_tac);                                   (* rewr. Den.   *)
 by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
                              addSEs evala_elim_cases)));
-bind_thm("aexp_iff", result() RS spec);
+qed_spec_mp "aexp_iff";
 
 goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B b s)";
 by (bexp.induct_tac "b" 1);
 by (ALLGOALS(asm_simp_tac (!simpset addcongs [conj_cong]
                                     addsimps (aexp_iff::evalb_simps))));
-bind_thm("bexp_iff", result() RS spec);
+qed_spec_mp "bexp_iff";
 
 val equiv_cs =
  comp_cs addss (simpset_of "Prod" addsimps (aexp_iff::bexp_iff::evalc.intrs));
 
-goal Equiv.thy "!!c. <c,s> -c-> t ==> (s,t) : C(c)";
+goal Equiv.thy "!c s t. <c,s> -c-> t --> (s,t) : C(c)";
 
 (* start with rule induction *)
-by (etac (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1);
+by (rtac evalc.mutual_induct 1);
 by (rewrite_tac (Gamma_def::C_simps));
   (* simplification with HOL_ss again too agressive *)
 (* skip *)
@@ -41,7 +41,7 @@
 by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
 by (fast_tac equiv_cs 1);
 
-qed "com1";
+qed_spec_mp "com1";
 
 
 goal Equiv.thy "!s t. (s,t):C(c) --> <c,s> -c-> t";
@@ -55,7 +55,7 @@
 by (rewtac Gamma_def);  
 by (fast_tac equiv_cs 1);
 
-bind_thm("com2", result() RS spec RS spec RS mp);
+qed_spec_mp "com2";
 
 
 (**** Proof of Equivalence ****)

--- a/src/HOL/IMP/Hoare.ML	Fri Feb 09 13:41:18 1996 +0100
+++ b/src/HOL/IMP/Hoare.ML	Fri Feb 09 13:41:59 1996 +0100
@@ -9,7 +9,7 @@
 
 open Hoare;
 
-goalw Hoare.thy [hoare_valid_def] "!P c Q. ({{P}}c{{Q}}) --> |= {{P}}c{{Q}}";
+goalw Hoare.thy [hoare_valid_def] "!P c Q. |- {P}c{Q} --> |= {P}c{Q}";
 by (rtac hoare.mutual_induct 1);
     by(ALLGOALS Asm_simp_tac);
   by(fast_tac rel_cs 1);
@@ -23,7 +23,7 @@
 by(eres_inst_tac [("x","a")] allE 1);
 by (safe_tac comp_cs);
   by(ALLGOALS Asm_full_simp_tac);
-qed "hoare_sound";
+qed_spec_mp "hoare_sound";
 
 goalw Hoare.thy [swp_def] "swp Skip Q = Q";
 by(Simp_tac 1);
@@ -68,11 +68,11 @@
 Delsimps [C_while];
 
 goalw Hoare.thy [hoare_valid_def,swp_def]
-  "!!c. |= {{P}}c{{Q}} ==> !s. P s --> swp c Q s";
+  "!!c. |= {P}c{Q} ==> !s. P s --> swp c Q s";
 by(fast_tac HOL_cs 1);
 qed "swp_is_weakest";
 
-goal Hoare.thy "!Q. {{swp c Q}} c {{Q}}";
+goal Hoare.thy "!Q. |- {swp c Q} c {Q}";
 by(com.induct_tac "c" 1);
 by(ALLGOALS Simp_tac);
     by(fast_tac (HOL_cs addIs [hoare.skip]) 1);
@@ -102,9 +102,9 @@
  by(Asm_full_simp_tac 1);
 by(rotate_tac ~1 1);
 by(Asm_full_simp_tac 1);
-bind_thm("swp_is_pre", result() RS spec);
+qed_spec_mp "swp_is_pre";
 
-goal Hoare.thy "!!c. |= {{P}}c{{Q}} ==> {{P}}c{{Q}}";
+goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
 br (swp_is_pre RSN (2,hoare.conseq)) 1;
  by(fast_tac HOL_cs 2);
 be swp_is_weakest 1;

--- a/src/HOL/IMP/Hoare.thy	Fri Feb 09 13:41:18 1996 +0100
+++ b/src/HOL/IMP/Hoare.thy	Fri Feb 09 13:41:59 1996 +0100
@@ -12,24 +12,24 @@
 
 consts
   hoare :: "(assn * com * assn) set"
-  hoare_valid :: [assn,com,assn] => bool ("|= {{_}}_{{_}}")
+  hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
 defs
-  hoare_valid_def "|= {{P}}c{{Q}} == !s t. (s,t) : C(c) --> P s --> Q t"
+  hoare_valid_def "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
 
-syntax "@hoare" :: [bool,com,bool] => bool ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
-translations "{{P}}c{{Q}}" == "(P,c,Q) : hoare"
+syntax "@hoare" :: [bool,com,bool] => bool ("|- {(1_)}/ (_)/ {(1_)}" 50)
+translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
 
 inductive "hoare"
 intrs
-  skip "{{P}}Skip{{P}}"
-  ass  "{{%s.P(s[A a s/x])}} x:=a {{P}}"
-  semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
-  If "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
-        {{P}} IF b THEN c ELSE d {{Q}}"
-  While "[| {{%s. P s & B b s}} c {{P}} |] ==>
-         {{P}} WHILE b DO c {{%s. P s & ~B b s}}"
-  conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
-          {{P'}}c{{Q'}}"
+  skip "|- {P}Skip{P}"
+  ass  "|- {%s.P(s[A a s/x])} x:=a {P}"
+  semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
+  If "[| |- {%s. P s & B b s}c{Q}; |- {%s. P s & ~B b s}d{Q} |] ==>
+      |- {P} IF b THEN c ELSE d {Q}"
+  While "|- {%s. P s & B b s} c {P} ==>
+         |- {P} WHILE b DO c {%s. P s & ~B b s}"
+  conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
+          |- {P'}c{Q'}"
 
 consts swp :: com => assn => assn
 defs swp_def "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"

--- a/src/HOL/IMP/VC.ML	Fri Feb 09 13:41:18 1996 +0100
+++ b/src/HOL/IMP/VC.ML	Fri Feb 09 13:41:59 1996 +0100
@@ -10,7 +10,7 @@
 
 val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[fast_tac HOL_cs 1]);
 
-goal VC.thy "!Q. (!s. vc c Q s) --> ({{wp c Q}} (astrip c) {{Q}})";
+goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}";
 by(acom.induct_tac "c" 1);
     by(ALLGOALS Simp_tac);
     by(fast_tac (HOL_cs addIs hoare.intrs) 1);
@@ -44,7 +44,7 @@
 by(EVERY1[rtac allI, rtac allI, rtac impI]);
 by(EVERY1[etac allE, etac allE, etac mp]);
 by(EVERY1[etac allE, etac allE, etac mp, atac]);
-bind_thm("wp_mono", result() RS spec RS spec RS mp RS spec RS mp);
+qed_spec_mp "wp_mono";
 
 goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
 by(acom.induct_tac "c" 1);
@@ -52,10 +52,10 @@
 by(safe_tac HOL_cs);
 by(EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
 by(fast_tac (HOL_cs addEs [wp_mono]) 1);
-bind_thm("vc_mono", result() RS spec RS spec RS mp RS spec RS mp);
+qed_spec_mp "vc_mono";
 
 goal VC.thy
-  "!P c Q. ({{P}}c{{Q}}) --> \
+  "!P c Q. |- {P}c{Q} --> \
 \          (? ac. astrip ac = c & (!s. P s --> wp ac Q s) & (!s. vc ac Q s))";
 by (rtac hoare.mutual_induct 1);
      by(res_inst_tac [("x","Askip")] exI 1);
@@ -76,7 +76,7 @@
 by(res_inst_tac [("x","ac")] exI 1);
 by(Asm_simp_tac 1);
 by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
-qed "vc_complete";
+qed_spec_mp "vc_complete";
 
 goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)";
 by(acom.induct_tac "c" 1);

--- a/src/HOL/Lambda/Eta.ML	Fri Feb 09 13:41:18 1996 +0100
+++ b/src/HOL/Lambda/Eta.ML	Fri Feb 09 13:41:59 1996 +0100
@@ -35,20 +35,20 @@
 by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
 by(nat_ind_tac "j1" 1);
 by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
-bind_thm("less_imp_pred_less",result() RS mp);
+qed_spec_mp "less_imp_pred_less";
 
 goal Arith.thy "i<j --> ~ pred j < i";
 by(nat_ind_tac "j" 1);
 by(ALLGOALS(asm_simp_tac(simpset_of "Arith")));
 by(fast_tac (HOL_cs addDs [less_imp_pred_less]) 1);
-bind_thm("less_imp_not_pred_less", result() RS mp);
+qed_spec_mp "less_imp_not_pred_less";
 Addsimps [less_imp_not_pred_less];
 
 goal Nat.thy "i < j --> j < Suc(Suc i) --> j = Suc i";
 by(nat_ind_tac "j" 1);
 by(ALLGOALS(simp_tac(simpset_of "Nat")));
 by(fast_tac (HOL_cs addDs [less_not_sym]) 1);
-bind_thm("less_interval1", result() RS mp RS mp);
+qed_spec_mp "less_interval1";
 
 
 (*** decr and free ***)
@@ -88,7 +88,7 @@
 goal Eta.thy "!!s. s -e> t ==> !i. free t i = free s i";
 by (etac (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1);
 by(ALLGOALS(asm_simp_tac (!simpset addsimps [decr_def] addcongs [conj_cong])));
-bind_thm("free_eta",result() RS spec);
+qed_spec_mp "free_eta";
 
 goal Eta.thy "!!s. [| s -e> t; ~free s i |] ==> ~free t i";
 by(asm_simp_tac (!simpset addsimps [free_eta]) 1);
@@ -99,7 +99,7 @@
 by(ALLGOALS(simp_tac (addsplit (!simpset))));
 by(fast_tac HOL_cs 1);
 by(fast_tac HOL_cs 1);
-bind_thm("subst_not_free", result() RS spec RS spec RS spec RS mp);
+qed_spec_mp "subst_not_free";
 
 goalw Eta.thy [decr_def] "!!s. ~free s i ==> s[t/i] = decr s i";
 by (etac subst_not_free 1);
@@ -109,7 +109,7 @@
 by (etac (eta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1);
 by(ALLGOALS(asm_simp_tac (!simpset addsimps [subst_subst RS sym,decr_def])));
 by(asm_simp_tac (!simpset addsimps [subst_decr]) 1);
-bind_thm("eta_subst",result() RS spec RS spec);
+qed_spec_mp "eta_subst";
 Addsimps [eta_subst];
 
 goalw Eta.thy [decr_def] "!!s. s -e> t ==> decr s i -e> decr t i";
@@ -154,12 +154,12 @@
 goal Eta.thy "!s t. s -> t --> (!i. free t i --> free s i)";
 by (rtac beta.mutual_induct 1);
 by(ALLGOALS(Asm_full_simp_tac));
-bind_thm("free_beta", result() RS spec RS spec RS mp RS spec RS mp);
+qed_spec_mp "free_beta";
 
 goalw Eta.thy [decr_def] "!s t. s -> t --> (!i. decr s i -> decr t i)";
 by (rtac beta.mutual_induct 1);
 by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [subst_subst RS sym])));
-bind_thm("beta_decr", result() RS spec RS spec RS mp RS spec);
+qed_spec_mp "beta_decr";
 
 goalw Eta.thy [decr_def]
   "decr (Var i) k = (if i<=k then Var i else Var(pred i))";
@@ -189,7 +189,7 @@
 by (rtac eta.mutual_induct 1);
 by(ALLGOALS(asm_simp_tac (addsplit (!simpset) addsimps [decr_def])));
 by(asm_simp_tac (addsplit (!simpset) addsimps [subst_decr]) 1);
-bind_thm("eta_lift",result() RS spec RS spec RS mp RS spec);
+qed_spec_mp "eta_lift";
 Addsimps [eta_lift];
 
 goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
@@ -198,7 +198,7 @@
 by(fast_tac (eta_cs addIs [r_into_rtrancl]) 1);
 by(fast_tac (eta_cs addSIs [rtrancl_eta_App]) 1);
 by(fast_tac (eta_cs addSIs [rtrancl_eta_Fun,eta_lift]) 1);
-bind_thm("rtrancl_eta_subst", result() RS spec RS spec RS spec RS mp);
+qed_spec_mp "rtrancl_eta_subst";
 
 goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)";
 by (rtac beta.mutual_induct 1);

--- a/src/HOL/Lambda/Lambda.ML	Fri Feb 09 13:41:18 1996 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Fri Feb 09 13:41:59 1996 +0100
@@ -102,7 +102,7 @@
 by (excluded_middle_tac "nat < i" 1);
 by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
 by (ALLGOALS(asm_full_simp_tac (addsplit(!simpset) addsimps [less_SucI])));
-bind_thm("lift_lift", result() RS spec RS spec RS mp);
+qed_spec_mp "lift_lift";
 
 goal Lambda.thy "!i j s. j < Suc i --> \
 \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
@@ -171,7 +171,7 @@
 by (Asm_simp_tac 1);
 by (forward_tac [lt_trans2] 1 THEN assume_tac 1);
 by (asm_simp_tac (!simpset addsimps [gt_pred]) 1);
-bind_thm("subst_subst", result() RS spec RS spec RS spec RS spec RS mp);
+qed_spec_mp "subst_subst";
 
 
 (*** Equivalence proof for optimized substitution ***)

--- a/src/HOL/Lambda/ParRed.ML	Fri Feb 09 13:41:18 1996 +0100
+++ b/src/HOL/Lambda/ParRed.ML	Fri Feb 09 13:41:59 1996 +0100
@@ -51,7 +51,7 @@
 goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n";
 by(db.induct_tac "t" 1);
 by(ALLGOALS(fast_tac (parred_cs addss (!simpset))));
-bind_thm("par_beta_lift", result() RS spec RS spec RS mp);
+qed_spec_mp "par_beta_lift";
 Addsimps [par_beta_lift];
 
 goal ParRed.thy
@@ -64,8 +64,7 @@
  by(asm_simp_tac (!simpset addsimps [subst_subst RS sym]) 1);
  by(fast_tac (parred_cs addSIs [par_beta_lift] addss (!simpset)) 1);
 by(fast_tac (parred_cs addss (!simpset)) 1);
-bind_thm("par_beta_subst",
-         result()  RS spec RS spec RS spec RS spec RS mp RS mp);
+qed_spec_mp "par_beta_subst";
 
 (*** Confluence (directly) ***)
 
@@ -83,7 +82,7 @@
  be rev_mp 1;
  by(db.induct_tac "db1" 1);
  by(ALLGOALS(fast_tac (parred_cs addSIs [par_beta_subst] addss (!simpset))));
-bind_thm("par_beta_cd", result() RS spec RS mp);
+qed_spec_mp "par_beta_cd";
 
 (*** Confluence (via cd) ***)
 

--- a/src/HOL/MiniML/I.ML	Fri Feb 09 13:41:18 1996 +0100
+++ b/src/HOL/MiniML/I.ML	Fri Feb 09 13:41:59 1996 +0100
@@ -63,7 +63,7 @@
 by (etac conjE 1);
 by (etac impE 1);
 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
-by ((dres_inst_tac [("xc","$ s a")] new_tv_W 1) THEN (atac 1));
+by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
     addss !simpset) 1);
 by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel])) 1);
@@ -78,7 +78,7 @@
 by (etac conjE 1);
 by (etac impE 1);
 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
-by ((dres_inst_tac [("xc","$ s a")] new_tv_W 1) THEN (atac 1));
+by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
     addss !simpset) 1);
 by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel,subst_comp_te])) 1);
@@ -90,7 +90,7 @@
 by (etac conjE 1);
 by (etac impE 1);
 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
-by ((dres_inst_tac [("xc","$ s a")] new_tv_W 1) THEN (atac 1));
+by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
     addss !simpset) 1);
 
@@ -107,7 +107,7 @@
 by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);
 by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
 by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
-by ((dres_inst_tac [("xc","$ s a")] new_tv_W 1) THEN (atac 1));
+by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
 by (safe_tac HOL_cs);
 by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
     addss !simpset) 1);
@@ -120,4 +120,4 @@
 by (fast_tac (HOL_cs addDs [new_tv_W] addss 
     (!simpset addsimps [subst_comp_tel])) 1);
 
-qed "I_correct_wrt_W";
+qed_spec_mp "I_correct_wrt_W";

--- a/src/HOL/MiniML/W.ML	Fri Feb 09 13:41:18 1996 +0100
+++ b/src/HOL/MiniML/W.ML	Fri Feb 09 13:41:59 1996 +0100
@@ -43,7 +43,7 @@
 by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
 by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,has_type_cl_sub,eq_sym_conv]) 1);
-qed "W_correct";
+qed_spec_mp "W_correct";
 
 val has_type_casesE = map(has_type.mk_cases expr.simps)
         [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
@@ -78,7 +78,7 @@
 by (res_inst_tac [("j","na")] le_trans 1); 
 by (Asm_simp_tac 1);
 by (asm_simp_tac (!simpset addsimps [Suc_leD]) 1);
-qed "W_var_ge";
+qed_spec_mp "W_var_ge";
 
 Addsimps [W_var_ge];
 
@@ -155,7 +155,7 @@
 by (fast_tac (HOL_cs addDs [W_var_geD] addIs
      [new_tv_list_le,new_tv_subst_tel,new_tv_le]
      addss (!simpset)) 1);
-bind_thm ("new_tv_W",result() RS spec RS spec RS spec RS spec RS spec RS mp RS mp);
+qed_spec_mp "new_tv_W";
 
 
 goal thy
@@ -215,11 +215,7 @@
     less_le_trans,subsetD]
   addEs [UnE]
   addss !simpset) 1); 
-bind_thm ("free_tv_W",result() RS spec RS spec RS spec RS spec RS spec RS spec RS mp RS mp RS mp); 
-
-goal HOL.thy "(~(P | Q)) = (~P & ~Q)";
-by( fast_tac HOL_cs 1);
-qed "not_disj"; 
+qed_spec_mp "free_tv_W"; 
 
 (* Completeness of W w.r.t. has_type *)
 goal thy
@@ -327,7 +323,7 @@
 by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
 by (dtac eq_subst_tel_eq_free 2);
 by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
-by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,not_disj]) 2);
+by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 2);
 
 by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 
 by (safe_tac HOL_cs );
@@ -353,7 +349,7 @@
 by (etac conjE 2);
 by (dtac new_tv_subst_tel 2);
 by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2);
-by (( forw_inst_tac [("xd","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
+by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));
 by (etac conjE 2);
 by (dtac (free_tv_app_subst_tel RS subsetD) 2);
 by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD,
@@ -366,14 +362,5 @@
 by (dtac (free_tv_app_subst_tel RS subsetD) 1);
 by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
     eq_subst_tel_eq_free] addss ((!simpset addsimps 
-    [not_disj,free_tv_subst,dom_def]))) 1);
-qed "W_complete";
-
-
-
-
-
-
-
-
-
+    [de_Morgan_disj,free_tv_subst,dom_def]))) 1);
+qed_spec_mp "W_complete";