1.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Wed Nov 24 13:35:31 1999 +0100
     1.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Wed Nov 24 13:36:14 1999 +0100
     1.3 @@ -97,17 +97,17 @@
     1.4  *};
     1.5  
     1.6  consts
     1.7 -  comp :: "('adr, 'val) expr => (('adr, 'val) instr) list";
     1.8 +  compile :: "('adr, 'val) expr => (('adr, 'val) instr) list";
     1.9  
    1.10  primrec
    1.11 -  "comp (Variable x) = [Load x]"
    1.12 -  "comp (Constant c) = [Const c]"
    1.13 -  "comp (Binop f e1 e2) = comp e2 @ comp e1 @ [Apply f]";
    1.14 +  "compile (Variable x) = [Load x]"
    1.15 +  "compile (Constant c) = [Const c]"
    1.16 +  "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]";
    1.17  
    1.18  
    1.19  text {*
    1.20    The main result of this development is the correctness theorem for
    1.21 -  $\idt{comp}$.  We first establish some lemmas about $\idt{exec}$.
    1.22 +  $\idt{compile}$.  We first establish some lemmas about $\idt{exec}$.
    1.23  *};
    1.24  
    1.25  lemma exec_append:
    1.26 @@ -128,8 +128,8 @@
    1.27    qed;
    1.28  qed;
    1.29  
    1.30 -lemma exec_comp:
    1.31 -  "ALL stack. exec (comp e) stack env =
    1.32 +lemma exec_compile:
    1.33 +  "ALL stack. exec (compile e) stack env =
    1.34      eval e env # stack" (is "?P e");
    1.35  proof (induct ?P e type: expr);
    1.36    fix adr; show "?P (Variable adr)"; by (simp!);
    1.37 @@ -143,7 +143,7 @@
    1.38  
    1.39  text {* Main theorem ahead. *};
    1.40  
    1.41 -theorem correctness: "execute (comp e) env = eval e env";
    1.42 -  by (simp add: execute_def exec_comp);
    1.43 +theorem correctness: "execute (compile e) env = eval e env";
    1.44 +  by (simp add: execute_def exec_compile);
    1.45  
    1.46  end;