# HG changeset patch
# User oheimb
# Date 905354749 -7200
# Node ID 506259e4e546e4ee2bbc4996704c808dddffd635
# Parent  3905974ad55514300f74817d6fb28943aae7c7b5
reflecting changes to Option.ML, List.{thy|ML}, mainly list_all

diff -r 3905974ad555 -r 506259e4e546 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Wed Sep 09 17:23:42 1998 +0200
+++ b/src/HOL/MiniML/Type.ML	Wed Sep 09 17:25:49 1998 +0200
@@ -348,8 +348,6 @@
 Goal "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
 by (induct_tac "sch" 1);
 by (ALLGOALS Asm_simp_tac);
-by (strip_tac 1);
-by (Fast_tac 1);
 qed "free_tv_ML_scheme";
 
 Goal "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
@@ -407,9 +405,7 @@
 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
 qed "new_tv_subst";
 
-Goal 
-  "new_tv n  = list_all (new_tv n)";
-by (rtac ext 1);
+Goal "new_tv n x = list_all (new_tv n) x";
 by (induct_tac "x" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_tv_list";
@@ -495,8 +491,6 @@
 Goal
   "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
 by (simp_tac (simpset() addsimps [new_tv_list]) 1);
-by (induct_tac "A" 1);
-by (ALLGOALS Asm_full_simp_tac);
 qed "new_tv_Suc_list";
 
 Goalw [new_tv_def] "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')";
diff -r 3905974ad555 -r 506259e4e546 src/HOL/W0/Type.ML
--- a/src/HOL/W0/Type.ML	Wed Sep 09 17:23:42 1998 +0200
+++ b/src/HOL/W0/Type.ML	Wed Sep 09 17:25:49 1998 +0200
@@ -146,9 +146,7 @@
 by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1);
 qed "new_tv_subst";
 
-Goal 
-  "new_tv n  = list_all (new_tv n)";
-by (rtac ext 1);
+Goal "new_tv n x = list_all (new_tv n) x";
 by (induct_tac "x" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_tv_list";
@@ -207,27 +205,23 @@
 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
 qed "new_tv_subst_var";
 
-Goal
-  "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
+Goal "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
 by (induct_tac "t" 1);
 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
 qed_spec_mp "new_tv_subst_te";
 Addsimps [new_tv_subst_te];
 
-Goal
-  "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
+Goal "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
 by (simp_tac (simpset() addsimps [new_tv_list]) 1);
 by (induct_tac "ts" 1);
-by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
+by (Safe_tac);
+by    (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
 qed_spec_mp "new_tv_subst_tel";
 Addsimps [new_tv_subst_tel];
 
 (* auxilliary lemma *)
-Goal
-  "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
+Goal "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
 by (simp_tac (simpset() addsimps [new_tv_list]) 1);
-by (induct_tac "ts" 1);
-by (ALLGOALS Asm_full_simp_tac);
 qed "new_tv_Suc_list";