# HG changeset patch
# User wenzelm
# Date 943446974 -3600
# Node ID 826c6222cca2fa475b9df4728ba7795ab9860947
# Parent  af8db187296040b56b21abd37b95289057ac1a13
renamed comp to compile (avoids clash with Relation.comp);

diff -r af8db1872960 -r 826c6222cca2 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Wed Nov 24 13:35:31 1999 +0100
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Wed Nov 24 13:36:14 1999 +0100
@@ -97,17 +97,17 @@
 *};
 
 consts
-  comp :: "('adr, 'val) expr => (('adr, 'val) instr) list";
+  compile :: "('adr, 'val) expr => (('adr, 'val) instr) list";
 
 primrec
-  "comp (Variable x) = [Load x]"
-  "comp (Constant c) = [Const c]"
-  "comp (Binop f e1 e2) = comp e2 @ comp e1 @ [Apply f]";
+  "compile (Variable x) = [Load x]"
+  "compile (Constant c) = [Const c]"
+  "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]";
 
 
 text {*
   The main result of this development is the correctness theorem for
-  $\idt{comp}$.  We first establish some lemmas about $\idt{exec}$.
+  $\idt{compile}$.  We first establish some lemmas about $\idt{exec}$.
 *};
 
 lemma exec_append:
@@ -128,8 +128,8 @@
   qed;
 qed;
 
-lemma exec_comp:
-  "ALL stack. exec (comp e) stack env =
+lemma exec_compile:
+  "ALL stack. exec (compile e) stack env =
     eval e env # stack" (is "?P e");
 proof (induct ?P e type: expr);
   fix adr; show "?P (Variable adr)"; by (simp!);
@@ -143,7 +143,7 @@
 
 text {* Main theorem ahead. *};
 
-theorem correctness: "execute (comp e) env = eval e env";
-  by (simp add: execute_def exec_comp);
+theorem correctness: "execute (compile e) env = eval e env";
+  by (simp add: execute_def exec_compile);
 
 end;