--- a/src/ZF/Coind/MT.ML Wed Jul 15 12:02:19 1998 +0200
+++ b/src/ZF/Coind/MT.ML Wed Jul 15 14:13:18 1998 +0200
@@ -11,22 +11,21 @@
(* The Consistency theorem *)
(* ############################################################ *)
-Goal
- "!!t. [| c:Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==> \
+Goal "[| c:Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==> \
\ <v_const(c), t> : HasTyRel";
by (Fast_tac 1);
qed "consistency_const";
Goalw [hastyenv_def]
- "!!t. [| x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> \
+ "[| x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> \
\ <ve_app(ve,x),t>:HasTyRel";
by (Fast_tac 1);
qed "consistency_var";
Goalw [hastyenv_def]
- "!!t. [| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te); \
+ "[| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te); \
\ <te,e_fn(x,e),t>:ElabRel \
\ |] ==> <v_clos(x, e, ve), t> : HasTyRel";
by (Best_tac 1);
@@ -143,8 +142,7 @@
fun mt_cases_tac t = ((rtac t 1) THEN (TRYALL assume_tac));
-Goal
- "!!e. <ve,e,v>:EvalRel ==> \
+Goal "<ve,e,v>:EvalRel ==> \
\ (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
by (etac EvalRel.induct 1);
by (safe_tac ZF_cs);