reflecting changes to Option.ML, List.{thy|ML}, mainly list_all
authoroheimb
Wed Sep 09 17:25:49 1998 +0200 (1998-09-09)
changeset 5446506259e4e546
parent 5445 3905974ad555
child 5447 df03d330aeab
reflecting changes to Option.ML, List.{thy|ML}, mainly list_all
src/HOL/MiniML/Type.ML
src/HOL/W0/Type.ML
     1.1 --- a/src/HOL/MiniML/Type.ML	Wed Sep 09 17:23:42 1998 +0200
     1.2 +++ b/src/HOL/MiniML/Type.ML	Wed Sep 09 17:25:49 1998 +0200
     1.3 @@ -348,8 +348,6 @@
     1.4  Goal "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
     1.5  by (induct_tac "sch" 1);
     1.6  by (ALLGOALS Asm_simp_tac);
     1.7 -by (strip_tac 1);
     1.8 -by (Fast_tac 1);
     1.9  qed "free_tv_ML_scheme";
    1.10  
    1.11  Goal "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
    1.12 @@ -407,9 +405,7 @@
    1.13  by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
    1.14  qed "new_tv_subst";
    1.15  
    1.16 -Goal 
    1.17 -  "new_tv n  = list_all (new_tv n)";
    1.18 -by (rtac ext 1);
    1.19 +Goal "new_tv n x = list_all (new_tv n) x";
    1.20  by (induct_tac "x" 1);
    1.21  by (ALLGOALS Asm_simp_tac);
    1.22  qed "new_tv_list";
    1.23 @@ -495,8 +491,6 @@
    1.24  Goal
    1.25    "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
    1.26  by (simp_tac (simpset() addsimps [new_tv_list]) 1);
    1.27 -by (induct_tac "A" 1);
    1.28 -by (ALLGOALS Asm_full_simp_tac);
    1.29  qed "new_tv_Suc_list";
    1.30  
    1.31  Goalw [new_tv_def] "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')";
     2.1 --- a/src/HOL/W0/Type.ML	Wed Sep 09 17:23:42 1998 +0200
     2.2 +++ b/src/HOL/W0/Type.ML	Wed Sep 09 17:25:49 1998 +0200
     2.3 @@ -146,9 +146,7 @@
     2.4  by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
     2.5  qed "new_tv_subst";
     2.6  
     2.7 -Goal 
     2.8 -  "new_tv n  = list_all (new_tv n)";
     2.9 -by (rtac ext 1);
    2.10 +Goal "new_tv n x = list_all (new_tv n) x";
    2.11  by (induct_tac "x" 1);
    2.12  by (ALLGOALS Asm_simp_tac);
    2.13  qed "new_tv_list";
    2.14 @@ -207,27 +205,23 @@
    2.15  by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
    2.16  qed "new_tv_subst_var";
    2.17  
    2.18 -Goal
    2.19 -  "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
    2.20 +Goal "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
    2.21  by (induct_tac "t" 1);
    2.22  by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
    2.23  qed_spec_mp "new_tv_subst_te";
    2.24  Addsimps [new_tv_subst_te];
    2.25  
    2.26 -Goal
    2.27 -  "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
    2.28 +Goal "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
    2.29  by (simp_tac (simpset() addsimps [new_tv_list]) 1);
    2.30  by (induct_tac "ts" 1);
    2.31 -by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
    2.32 +by (Safe_tac);
    2.33 +by    (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
    2.34  qed_spec_mp "new_tv_subst_tel";
    2.35  Addsimps [new_tv_subst_tel];
    2.36  
    2.37  (* auxilliary lemma *)
    2.38 -Goal
    2.39 -  "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
    2.40 +Goal "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
    2.41  by (simp_tac (simpset() addsimps [new_tv_list]) 1);
    2.42 -by (induct_tac "ts" 1);
    2.43 -by (ALLGOALS Asm_full_simp_tac);
    2.44  qed "new_tv_Suc_list";
    2.45  
    2.46