# HG changeset patch
# User wenzelm
# Date 931451948 -7200
# Node ID 914233d95b23160cd7f31aeee72fafd3a6f617d2
# Parent  d9e3e2b30bee065076d0adb1e955f066699ad35f
tuned indentation;

diff -r d9e3e2b30bee -r 914233d95b23 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Thu Jul 08 18:37:54 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Thu Jul 08 18:39:08 1999 +0200
@@ -109,9 +109,9 @@
   show "??P (x # xs)" (is "??Q x");
   proof (induct ??Q x type: instr);
     fix val; show "??Q (Const val)"; by brute_force;
-    next;
+  next;
     fix adr; show "??Q (Load adr)"; by brute_force;
-    next;
+  next;
     fix fun; show "??Q (Apply fun)"; by brute_force;
   qed;
 qed;
@@ -119,11 +119,10 @@
 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 brute_force;
-  next;
+next;
   fix val; show "??P (Constant val)"; by brute_force;
-  next;
+next;
   fix fun e1 e2; assume "??P e1" "??P e2"; show "??P (Binop fun e1 e2)";
     by (brute_force simp add: exec_append);
 qed;