--- a/src/HOL/W0/I.ML Thu Aug 20 16:18:39 1998 +0200
+++ b/src/HOL/W0/I.ML Thu Aug 20 16:20:17 1998 +0200
@@ -8,8 +8,7 @@
open I;
-Goal
- "! a m s s' t n. \
+Goal "! a m s s' t n. \
\ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \
\ ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
by (induct_tac "e" 1);
@@ -123,8 +122,7 @@
(***
We actually want the corollary
-Goal
- "I e [] m id_subst = Ok(s,t,n) --> W e [] m = Ok(s, $s t, n)";
+Goal "I e [] m id_subst = Ok(s,t,n) --> W e [] m = Ok(s, $s t, n)";
by (cut_facts_tac [(read_instantiate[("x","id_subst")]
(read_instantiate[("x","[]")](thm RS spec)
RS spec RS spec))] 1);