--- a/src/HOL/Isar_examples/W_correct.thy Thu Aug 17 10:33:37 2000 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy Thu Aug 17 10:34:11 2000 +0200
@@ -126,7 +126,7 @@
by (simp add: subst_comp_tel o_def);
show "$s a |- e1 :: $ u t2 -> t";
proof -;
- from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1";
+ from hyp1 W1_ok [symmetric]; have "$ s1 a |- e1 :: t1";
by blast;
hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)";
by (intro has_type_subst_closed);
@@ -134,7 +134,7 @@
qed;
show "$ s a |- e2 :: $ u t2";
proof -;
- from hyp2 W2_ok [RS sym];
+ from hyp2 W2_ok [symmetric];
have "$ s2 ($ s1 a) |- e2 :: t2"; by blast;
hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2";
by (rule has_type_subst_closed);
@@ -143,7 +143,7 @@
qed;
};
qed;
- with W_ok [RS sym]; show ?thesis; by blast;
+ with W_ok [symmetric]; show ?thesis; by blast;
qed;
end;