# HG changeset patch # User wenzelm # Date 939394064 -7200 # Node ID c3e6f27bfcb7df4221f8cb584444cd5af583a578 # Parent fd019ac3485fa6f8e309007e84d0ba7799f43d48 tuned presentation; diff -r fd019ac3485f -r c3e6f27bfcb7 src/HOL/Isar_examples/W_correct.thy --- a/src/HOL/Isar_examples/W_correct.thy Fri Oct 08 16:40:27 1999 +0200 +++ b/src/HOL/Isar_examples/W_correct.thy Fri Oct 08 16:47:44 1999 +0200 @@ -143,8 +143,8 @@ qed; show "$ s a |- e2 :: $ u t2"; proof -; - from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2"; - by blast; + from hyp2 W2_ok [RS sym]; + have "$ s2 ($ s1 a) |- e2 :: t2"; by blast; hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"; by (rule has_type_subst_closed); with s'; show ?thesis; by simp;