tuned presentation;
authorwenzelm
Fri Oct 08 16:47:44 1999 +0200 (1999-10-08)
changeset 7809c3e6f27bfcb7
parent 7808 fd019ac3485f
child 7810 e5f15a673a69
tuned presentation;
src/HOL/Isar_examples/W_correct.thy
     1.1 --- a/src/HOL/Isar_examples/W_correct.thy	Fri Oct 08 16:40:27 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Fri Oct 08 16:47:44 1999 +0200
     1.3 @@ -143,8 +143,8 @@
     1.4            qed;
     1.5            show "$ s a |- e2 :: $ u t2";
     1.6            proof -;
     1.7 -            from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2";
     1.8 -              by blast;
     1.9 +            from hyp2 W2_ok [RS sym];
    1.10 +              have "$ s2 ($ s1 a) |- e2 :: t2"; by blast;
    1.11              hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2";
    1.12                by (rule has_type_subst_closed);
    1.13              with s'; show ?thesis; by simp;