--- a/src/HOL/Isar_examples/ExprCompiler.thy Sat Sep 04 21:12:15 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy Sat Sep 04 21:13:01 1999 +0200
@@ -100,30 +100,30 @@
*};
lemma exec_append:
- "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs");
-proof (induct ??P xs type: list);
- show "??P []"; by simp;
+ "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "?P xs");
+proof (induct ?P xs type: list);
+ show "?P []"; by simp;
fix x xs;
- assume "??P xs";
- show "??P (x # xs)" (is "??Q x");
- proof (induct ??Q x type: instr);
- fix val; show "??Q (Const val)"; by force;
+ assume "?P xs";
+ show "?P (x # xs)" (is "?Q x");
+ proof (induct ?Q x type: instr);
+ fix val; show "?Q (Const val)"; by force;
next;
- fix adr; show "??Q (Load adr)"; by force;
+ fix adr; show "?Q (Load adr)"; by force;
next;
- fix fun; show "??Q (Apply fun)"; by force;
+ fix fun; show "?Q (Apply fun)"; by force;
qed;
qed;
lemma exec_comp:
- "ALL stack. exec (comp e) stack env = eval e env # stack" (is "??P e");
-proof (induct ??P e type: expr);
- fix adr; show "??P (Variable adr)"; by force;
+ "ALL stack. exec (comp e) stack env = eval e env # stack" (is "?P e");
+proof (induct ?P e type: expr);
+ fix adr; show "?P (Variable adr)"; by force;
next;
- fix val; show "??P (Constant val)"; by force;
+ fix val; show "?P (Constant val)"; by force;
next;
- fix fun e1 e2; assume "??P e1" "??P e2"; show "??P (Binop fun e1 e2)";
+ fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)";
by (force simp add: exec_append);
qed;