src/HOL/ex/MT.ML
changeset 3842 b55686a7b22c
parent 2935 998cb95fdd43
child 4089 96fba19bcbe2
     1.1 --- a/src/HOL/ex/MT.ML	Fri Oct 10 18:37:49 1997 +0200
     1.2 +++ b/src/HOL/ex/MT.ML	Fri Oct 10 19:02:28 1997 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4  qed "lfp_elim2";
     1.5  
     1.6  val prems = goal MT.thy
     1.7 -  " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \
     1.8 +  " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \
     1.9  \   P(x)";
    1.10  by (cut_facts_tac prems 1);
    1.11  by (etac induct 1);
    1.12 @@ -446,7 +446,7 @@
    1.13  val prems = goal MT.thy 
    1.14    " te |- e ===> t ==> \
    1.15  \   ( e = fn x1 => e1 --> \
    1.16 -\     (? t1 t2.t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
    1.17 +\     (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
    1.18  \   )";
    1.19  by (elab_e_elim_tac prems);
    1.20  qed "elab_fn_elim_lem";
    1.21 @@ -538,11 +538,11 @@
    1.22  (* Elimination rule for hasty_rel *)
    1.23  
    1.24  val prems = goalw MT.thy [hasty_rel_def]
    1.25 -  " [| !! c t.c isof t ==> P((v_const(c),t)); \
    1.26 +  " [| !! c t. c isof t ==> P((v_const(c),t)); \
    1.27  \      !! te ev e t ve. \
    1.28  \        [| te |- fn ev => e ===> t; \
    1.29  \           ve_dom(ve) = te_dom(te); \
    1.30 -\           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
    1.31 +\           !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
    1.32  \        |] ==> P((v_clos(<|ev,e,ve|>),t)); \
    1.33  \      (v,t) : hasty_rel \
    1.34  \   |] ==> P((v,t))";
    1.35 @@ -558,11 +558,11 @@
    1.36  
    1.37  val prems = goal MT.thy 
    1.38    " [| (v,t) : hasty_rel; \
    1.39 -\      !! c t.c isof t ==> P (v_const c) t; \
    1.40 +\      !! c t. c isof t ==> P (v_const c) t; \
    1.41  \      !! te ev e t ve. \
    1.42  \        [| te |- fn ev => e ===> t; \
    1.43  \           ve_dom(ve) = te_dom(te); \
    1.44 -\           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
    1.45 +\           !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
    1.46  \        |] ==> P (v_clos <|ev,e,ve|>) t \
    1.47  \   |] ==> P v t";
    1.48  by (res_inst_tac [("P","P")] infsys_p2 1);
    1.49 @@ -602,7 +602,7 @@
    1.50  val prems = goalw MT.thy [hasty_env_def,hasty_def] 
    1.51    " v hasty t ==> \
    1.52  \   ! x e ve. \
    1.53 -\     v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
    1.54 +\     v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)";
    1.55  by (cut_facts_tac prems 1);
    1.56  by (rtac hasty_rel_elim 1);
    1.57  by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
    1.58 @@ -610,7 +610,7 @@
    1.59  
    1.60  goal MT.thy 
    1.61    "!!t. v_clos(<|ev,e,ve|>) hasty t ==>  \
    1.62 -\       ? te.te |- fn ev => e ===> t & ve hastyenv te ";
    1.63 +\       ? te. te |- fn ev => e ===> t & ve hastyenv te ";
    1.64  by (dtac hasty_elim_clos_lem 1);
    1.65  by (Blast_tac 1);
    1.66  qed "hasty_elim_clos";