Some lemmas changed to valuesd

--- a/src/HOL/MiniML/Generalize.thy	Fri Feb 14 15:32:00 1997 +0100
+++ b/src/HOL/MiniML/Generalize.thy	Fri Feb 14 16:01:43 1997 +0100
@@ -9,7 +9,7 @@
 Generalize = Instance +
 
 
-(* gen: binding (generalising) the variables which are not free in the type scheme *)
+(* gen: binding (generalising) the variables which are not free in the context *)
 
 types ctxt = type_scheme list
     
@@ -18,7 +18,7 @@
 
 primrec gen typ
   "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
-  "gen A (t1 -> t2) = ((gen A t1) =-> (gen A t2))"
+  "gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
 
 (* executable version of gen: Implementation with free_tv_ML *)
 
@@ -27,7 +27,7 @@
 
 primrec gen_ML_aux typ
   "gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
-  "gen_ML_aux A (t1 -> t2) = ((gen_ML_aux A t1) =-> (gen_ML_aux A t2))"
+  "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
 
 consts
   gen_ML :: [ctxt, typ] => type_scheme

--- a/src/HOL/MiniML/Instance.ML	Fri Feb 14 15:32:00 1997 +0100
+++ b/src/HOL/MiniML/Instance.ML	Fri Feb 14 16:01:43 1997 +0100
@@ -15,6 +15,7 @@
 qed "bound_typ_inst_mk_scheme";
 
 Addsimps [bound_typ_inst_mk_scheme];
+
 goal thy "!!S. bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
 by (type_scheme.induct_tac "sch" 1);
 by (ALLGOALS Asm_full_simp_tac);
@@ -27,6 +28,7 @@
 qed "bound_typ_inst_eq";
 
 
+
 (* lemmatas for bound_scheme_inst *)
 
 goal thy "!!t. bound_scheme_inst B (mk_scheme t) = mk_scheme t";

--- a/src/HOL/MiniML/Maybe.ML	Fri Feb 14 15:32:00 1997 +0100
+++ b/src/HOL/MiniML/Maybe.ML	Fri Feb 14 16:01:43 1997 +0100
@@ -23,9 +23,14 @@
 by (Asm_simp_tac 1);
 qed "expand_option_bind";
 
-goal Maybe.thy
+goal thy
   "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
 by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
 qed "option_bind_eq_None";
 
 Addsimps [option_bind_eq_None];
+
+(* auxiliary lemma *)
+goal Maybe.thy "(y = Some x) = (Some x = y)";
+by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
+qed "rotate_Some";

--- a/src/HOL/MiniML/Type.ML	Fri Feb 14 15:32:00 1997 +0100
+++ b/src/HOL/MiniML/Type.ML	Fri Feb 14 16:01:43 1997 +0100
@@ -16,7 +16,7 @@
 by (Fast_tac 1);
 qed_spec_mp "mk_scheme_Fun";
 
-goal Type.thy "!t'.mk_scheme t = mk_scheme t' --> t=t'";
+goal thy "!t'.mk_scheme t = mk_scheme t' --> t=t'";
 by (typ.induct_tac "t" 1);
  br allI 1;
  by (typ.induct_tac "t'" 1);
@@ -96,19 +96,33 @@
 by (fast_tac (HOL_cs addss !simpset) 1);
 qed "new_tv_Cons";
 
-goalw Type.thy [new_tv_def] "!!n. new_tv n TVar";
+goalw thy [new_tv_def] "!!n. new_tv n TVar";
 by (strip_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1);
 qed "new_tv_TVar_subst";
 
 Addsimps [new_tv_TVar,new_tv_FVar,new_tv_BVar,new_tv_Fun,new_tv_Fun2,new_tv_Nil,new_tv_Cons,new_tv_TVar_subst];
 
-goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
+goalw thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
   "new_tv n id_subst";
 by(Simp_tac 1);
 qed "new_tv_id_subst";
 Addsimps[new_tv_id_subst];
 
+goal thy "new_tv n (sch::type_scheme) --> \
+\              $(%k.if k<n then S k else S' k) sch = $S sch";
+by (type_scheme.induct_tac "sch" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "new_if_subst_type_scheme";
+Addsimps [new_if_subst_type_scheme];
+
+goal thy "new_tv n (A::type_scheme list) --> \
+\              $(%k.if k<n then S k else S' k) A = $S A";
+by (list.induct_tac "A" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "new_if_subst_type_scheme_list";
+Addsimps [new_if_subst_type_scheme_list];
+
 
 (* constructor laws for dom and cod *)
 
@@ -542,7 +556,7 @@
 goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (fast_tac (!claset addDs [not_leE] addIs [less_trans]) 1);
-qed "less_maxR";
+val less_maxR = result();
 
 goalw thy [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
 by (typ.induct_tac "t" 1);
@@ -574,12 +588,12 @@
 
 goalw thy [max_def] "!!n::nat. n <= (max n n')";
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-qed "le_maxL";
+val le_maxL = result();
 
 goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (fast_tac (!claset addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
-qed "le_maxR";
+val le_maxR = result();
 
 goal thy "!!A::type_scheme list. ? n. (new_tv n A)";
 by (list.induct_tac "A" 1);

--- a/src/HOL/MiniML/Type.thy	Fri Feb 14 15:32:00 1997 +0100
+++ b/src/HOL/MiniML/Type.thy	Fri Feb 14 16:01:43 1997 +0100
@@ -54,6 +54,7 @@
   "free_tv [] = {}"
   "free_tv (x#l) = (free_tv x) Un (free_tv l)"
 
+  
 (* executable version of free_tv: Implementation with lists *)
 consts
   free_tv_ML :: ['a::type_struct] => nat list

--- a/src/HOL/MiniML/W.ML	Fri Feb 14 15:32:00 1997 +0100
+++ b/src/HOL/MiniML/W.ML	Fri Feb 14 16:01:43 1997 +0100
@@ -74,11 +74,6 @@
 ba 1;
 qed "new_tv_compatible_W";
 
-(* auxiliary lemma *)
-goal Maybe.thy "(y = Some x) = (Some x = y)";
-by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
-qed "rotate_Some";
-
 goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
 by (type_scheme.induct_tac "sch" 1);
 by (Asm_full_simp_tac 1);
@@ -335,11 +330,11 @@
 
 goal thy "!!A. (!x. x : A --> x ~: B) ==> A Int B = {}";
 by (Fast_tac 1);
-qed "weaken_A_Int_B_eq_empty";
+val weaken_A_Int_B_eq_empty = result();
 
 goal thy "!!A. x ~: A | x : B ==> x ~: A - B";
 by (Fast_tac 1);
-qed "weaken_not_elem_A_minus_B";
+val weaken_not_elem_A_minus_B = result();
 
 (* correctness of W with respect to has_type *)
 goal W.thy
@@ -462,25 +457,11 @@
 by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1);
 qed_spec_mp "W_correct_lemma";
 
-goal Type.thy "new_tv n (sch::type_scheme) --> \
-\              $(%k.if k<n then S k else S' k) sch = $S sch";
-by (type_scheme.induct_tac "sch" 1);
-by(ALLGOALS Asm_simp_tac);
-qed "new_if_subst_type_scheme";
-Addsimps [new_if_subst_type_scheme];
-
-goal Type.thy "new_tv n (A::type_scheme list) --> \
-\              $(%k.if k<n then S k else S' k) A = $S A";
-by (list.induct_tac "A" 1);
-by(ALLGOALS Asm_simp_tac);
-qed "new_if_subst_type_scheme_list";
-Addsimps [new_if_subst_type_scheme_list];
-
 goal Arith.thy "!!n::nat. ~ k+n < n";
 by (nat_ind_tac "k" 1);
 by(ALLGOALS Asm_simp_tac);
 by(trans_tac 1);
-qed "not_add_less1";
+val not_add_less1 = result();
 Addsimps [not_add_less1];
 
 (* Completeness of W w.r.t. has_type *)