# HG changeset patch
# User paulson
# Date 903622817 -7200
# Node ID eab069aa1ad0fbf9fa7be5ddf7c12a759a13ea05
# Parent  5f6416d64a947dc4fc3af6d085950a567a4738cf
tidied

diff -r 5f6416d64a94 -r eab069aa1ad0 src/HOL/W0/I.ML
--- 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);