src/HOL/Isar_examples/ExprCompiler.thy
changeset 13524 604d0f3622d6
parent 11809 c9ffdd63dd93
child 13537 f506eb568121
     1.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4   better idea of what is actually going on.
     1.5  *}
     1.6  
     1.7 -lemma exec_append:
     1.8 +lemma exec_append':
     1.9    "ALL stack. exec (xs @ ys) stack env
    1.10      = exec ys (exec xs stack env) env" (is "?P xs")
    1.11  proof (induct xs)