author wenzelm Thu, 16 Mar 2000 00:36:22 +0100 changeset 8491 82826ed95d4b parent 8490 6e0f23304061 child 8492 6343c725ba7e
Splitter support;
--- a/src/HOL/Isar_examples/W_correct.thy	Thu Mar 16 00:35:27 2000 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy	Thu Mar 16 00:36:22 2000 +0100
@@ -90,13 +90,6 @@

subsection {* Correctness theorem *};

-text_raw {* \begin{comment} *};
-
-(* FIXME proper split att/mod *)
-ML_setup {* Addsplits [split_bind]; *};
-
-text_raw {* \end{comment} *};
-
theorem W_correct: "W e a n = Ok (s, t, m) ==> $s a |- e :: t"; proof -; assume W_ok: "W e a n = Ok (s, t, m)"; @@ -112,7 +105,7 @@ assume "Ok (s, t, m) = W (Abs e) a n"; thus "$ s a |- Abs e :: t";
obtain t' where "t = s n -> t'" "Ok (s, t', m) = W e (TVar n # a) (Suc n)";
-	  by (rule rev_mp) simp;
+	  by (rule rev_mp) (simp split: split_bind);
with hyp; show ?thesis; by (force intro: has_type.Abs);
qed;
qed;
@@ -128,7 +121,7 @@
and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u" and W1_ok: "W e1 a n = Ok (s1, t1, n1)" and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)";
-	    by (rule rev_mp) simp;
+	    by (rule rev_mp) (simp split: split_bind);
show ?thesis;
proof (rule has_type.App);
from s; have s': "$u ($ s2 ($s1 a)) =$s a";