src/HOL/MiniML/MiniML.ML

--- a/src/HOL/MiniML/MiniML.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/MiniML/MiniML.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -10,21 +10,21 @@
 Addsimps [is_bound_typ_instance_closed_subst];
 
 
-goal thy "!!t::typ. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t = $S t";
+Goal "!!t::typ. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t = $S t";
 by (rtac typ_substitutions_only_on_free_variables 1);
 by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1);
 qed "s'_t_equals_s_t";
 
 Addsimps [s'_t_equals_s_t];
 
-goal thy "!!A::type_scheme list. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A = $S A";
+Goal "!!A::type_scheme list. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A = $S A";
 by (rtac scheme_list_substitutions_only_on_free_variables 1);
 by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1);
 qed "s'_a_equals_s_a";
 
 Addsimps [s'_a_equals_s_a];
 
-goal thy "!!S.($ (%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A |- e :: \ 
+Goal "!!S.($ (%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A |- e :: \ 
 \              $ (%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t) ==> \
 \             $S A |- e :: $S t";
 
@@ -35,38 +35,38 @@
 by (Asm_full_simp_tac 1);
 qed "replace_s_by_s'";
 
-goal thy "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = $ id_subst A";
+Goal "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = $ id_subst A";
 by (rtac scheme_list_substitutions_only_on_free_variables 1);
 by (asm_full_simp_tac (simpset() addsimps [id_subst_def]) 1);
 qed "alpha_A'";
 
-goal thy "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = A";
+Goal "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = A";
 by (rtac (alpha_A' RS ssubst) 1);
 by (Asm_full_simp_tac 1);
 qed "alpha_A";
 
-goal thy "!!alpha. $ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
+Goal "!!alpha. $ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
 by (typ.induct_tac "t" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 qed "S_o_alpha_typ";
 
-goal thy "!!alpha. $ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
+Goal "!!alpha. $ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
 by (typ.induct_tac "t" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 val S_o_alpha_typ' = result ();
 
-goal thy "!!alpha. $ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)";
+Goal "!!alpha. $ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)";
 by (type_scheme.induct_tac "sch" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 qed "S_o_alpha_type_scheme";
 
-goal thy "!!alpha. $ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)";
+Goal "!!alpha. $ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)";
 by (list.induct_tac "A" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 by (rtac (rewrite_rule [o_def] S_o_alpha_type_scheme) 1);
 qed "S_o_alpha_type_scheme_list";
 
-goal thy "!!A::type_scheme list. \
+Goal "!!A::type_scheme list. \
 \              ($ (%n. if n : free_tv A Un free_tv t \
 \                      then S n else TVar n) \
 \                 A) = \
@@ -79,14 +79,14 @@
 by (rtac refl 1);
 qed "S'_A_eq_S'_alpha_A";
 
-goalw thy [free_tv_subst,dom_def]
+Goalw [free_tv_subst,dom_def]
           "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
 \               free_tv A Un free_tv t";
 by (Simp_tac 1);
 by (Fast_tac 1);
 qed "dom_S'";
 
-goalw thy [free_tv_subst,cod_def,subset_def]
+Goalw [free_tv_subst,cod_def,subset_def]
           "!!(A::type_scheme list) (t::typ). \ 
 \              cod (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
 \              free_tv ($ S A) Un free_tv ($ S t)";
@@ -99,14 +99,14 @@
                       addIs [free_tv_of_substitutions_extend_to_types RS subsetD]) 1);
 qed "cod_S'";
 
-goalw thy [free_tv_subst]
+Goalw [free_tv_subst]
           "!!(A::type_scheme list) (t::typ). \
 \               free_tv (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
 \               free_tv A Un free_tv ($ S A) Un free_tv t Un free_tv ($ S t)";
 by (fast_tac (claset() addDs [dom_S' RS subsetD,cod_S' RS subsetD]) 1);
 qed "free_tv_S'";
 
-goal thy "!!t1::typ. \
+Goal "!!t1::typ. \
 \         (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
 \         {x. ? y. x = n + y}";
 by (typ.induct_tac "t1" 1);
@@ -116,7 +116,7 @@
 by (Fast_tac 1);
 qed "free_tv_alpha";
 
-goal thy "!!(k::nat). n <= n + k";
+Goal "!!(k::nat). n <= n + k";
 by (res_inst_tac [("n","k")] nat_induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
@@ -124,7 +124,7 @@
 
 Addsimps [aux_plus];
 
-goal thy "!!t::typ. new_tv n t ==> {x. ? y. x = n + y} Int free_tv t = {}";
+Goal "!!t::typ. new_tv n t ==> {x. ? y. x = n + y} Int free_tv t = {}";
 by Safe_tac;
 by (cut_facts_tac [aux_plus] 1);
 by (dtac new_tv_le 1);
@@ -134,7 +134,7 @@
 by (Fast_tac 1);
 val new_tv_Int_free_tv_empty_type = result ();
 
-goal thy "!!sch::type_scheme. new_tv n sch ==> {x. ? y. x = n + y} Int free_tv sch = {}";
+Goal "!!sch::type_scheme. new_tv n sch ==> {x. ? y. x = n + y} Int free_tv sch = {}";
 by Safe_tac;
 by (cut_facts_tac [aux_plus] 1);
 by (dtac new_tv_le 1);
@@ -144,7 +144,7 @@
 by (Fast_tac 1);
 val new_tv_Int_free_tv_empty_scheme = result ();
 
-goal thy "!!n. !A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}";
+Goal "!!n. !A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}";
 by (rtac allI 1);
 by (list.induct_tac "A" 1);
 by (Simp_tac 1);
@@ -152,7 +152,7 @@
 by (fast_tac (claset() addDs [new_tv_Int_free_tv_empty_scheme ]) 1);
 val new_tv_Int_free_tv_empty_scheme_list = result ();
 
-goalw thy [le_type_scheme_def,is_bound_typ_instance] 
+Goalw [le_type_scheme_def,is_bound_typ_instance] 
       "!!A. new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
 by (strip_tac 1);
 by (etac exE 1);
@@ -174,7 +174,7 @@
 
 AddSIs has_type.intrs;
 
-goal thy "!!e. A |- e::t ==> !B. A <= B -->  B |- e::t";
+Goal "!!e. A |- e::t ==> !B. A <= B -->  B |- e::t";
 by (etac has_type.induct 1);
    by (simp_tac (simpset() addsimps [le_env_def]) 1);
    by (fast_tac (claset() addEs [bound_typ_instance_trans] addss simpset()) 1);
@@ -184,7 +184,7 @@
 qed_spec_mp "has_type_le_env";
 
 (* has_type is closed w.r.t. substitution *)
-goal thy "!!a. A |- e :: t ==> !S. $S A |- e :: $S t";
+Goal "!!a. A |- e :: t ==> !S. $S A |- e :: $S t";
 by (etac has_type.induct 1);
 (* case VarI *)
    by (rtac allI 1);