# HG changeset patch
# User nipkow
# Date 1021024586 -7200
# Node ID 423ce375bf6509b2b08e85dcbcf0d40472fb328b
# Parent  bb448fb7519182316348100adbc3979b0ab64dd5
commented out half converted proof

diff -r bb448fb75191 -r 423ce375bf65 src/HOL/IMP/Compiler0.thy
--- 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