commented out half converted proof
authornipkow
Fri May 10 11:56:26 2002 +0200 (2002-05-10)
changeset 13130423ce375bf65
parent 13129 bb448fb75191
child 13131 2d284f0dfd56
commented out half converted proof
src/HOL/IMP/Compiler0.thy
     1.1 --- a/src/HOL/IMP/Compiler0.thy	Fri May 10 11:55:45 2002 +0200
     1.2 +++ b/src/HOL/IMP/Compiler0.thy	Fri May 10 11:56:26 2002 +0200
     1.3 @@ -215,7 +215,7 @@
     1.4    Second proof; statement is generalized to cater for prefixes and suffixes;
     1.5    needs none of the lifting lemmas, but instantiations of pre/suffix.
     1.6    *}
     1.7 -
     1.8 +(*
     1.9  theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    1.10  shows "\<And>a z. a@compile c@z \<turnstile> \<langle>s,size a\<rangle> -*\<rightarrow> \<langle>t,size a + size(compile c)\<rangle>"
    1.11        (is "\<And>a z. ?P c s t a z")
    1.12 @@ -269,7 +269,7 @@
    1.13   apply(force intro!: JMPB)
    1.14  apply(simp)
    1.15  done
    1.16 -
    1.17 +*)
    1.18  text {* Missing: the other direction! I did much of it, and although
    1.19  the main lemma is very similar to the one in the new development, the
    1.20  lemmas surrounding it seemed much more complicated. In the end I gave