--- a/src/HOL/IMP/Compiler0.thy Fri May 10 11:55:45 2002 +0200
+++ b/src/HOL/IMP/Compiler0.thy Fri May 10 11:56:26 2002 +0200
@@ -215,7 +215,7 @@
Second proof; statement is generalized to cater for prefixes and suffixes;
needs none of the lifting lemmas, but instantiations of pre/suffix.
*}
-
+(*
theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
shows "\<And>a z. a@compile c@z \<turnstile> \<langle>s,size a\<rangle> -*\<rightarrow> \<langle>t,size a + size(compile c)\<rangle>"
(is "\<And>a z. ?P c s t a z")
@@ -269,7 +269,7 @@
apply(force intro!: JMPB)
apply(simp)
done
-
+*)
text {* Missing: the other direction! I did much of it, and although
the main lemma is very similar to the one in the new development, the
lemmas surrounding it seemed much more complicated. In the end I gave