src/HOL/Isar_examples/ExprCompiler.thy
changeset 13537 f506eb568121
parent 13524 604d0f3622d6
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 15:39:39 2002 +0200
     1.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Aug 27 15:40:33 2002 +0200
     1.3 @@ -197,7 +197,7 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -theorem correctness: "execute (compile e) env = eval e env"
     1.8 +theorem correctness': "execute (compile e) env = eval e env"
     1.9  proof -
    1.10    have exec_compile:
    1.11      "ALL stack. exec (compile e) stack env = eval e env # stack"