src/HOL/Isar_examples/ExprCompiler.thy
changeset 7565 bfa85f429629
parent 7480 0a0e0dbe1269
child 7740 2fbe5ce9845f
     1.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Sep 21 17:30:11 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Sep 21 17:30:55 1999 +0200
     1.3 @@ -108,23 +108,23 @@
     1.4    assume "?P xs";
     1.5    show "?P (x # xs)" (is "?Q x");
     1.6    proof (induct ?Q x type: instr);
     1.7 -    fix val; show "?Q (Const val)"; by force;
     1.8 +    fix val; show "?Q (Const val)"; by (simp!);
     1.9    next;
    1.10 -    fix adr; show "?Q (Load adr)"; by force;
    1.11 +    fix adr; show "?Q (Load adr)"; by (simp!);
    1.12    next;
    1.13 -    fix fun; show "?Q (Apply fun)"; by force;
    1.14 +    fix fun; show "?Q (Apply fun)"; by (simp!);
    1.15    qed;
    1.16  qed;
    1.17  
    1.18  lemma exec_comp:
    1.19    "ALL stack. exec (comp e) stack env = eval e env # stack" (is "?P e");
    1.20  proof (induct ?P e type: expr);
    1.21 -  fix adr; show "?P (Variable adr)"; by force;
    1.22 +  fix adr; show "?P (Variable adr)"; by (simp!);
    1.23  next;
    1.24 -  fix val; show "?P (Constant val)"; by force;
    1.25 +  fix val; show "?P (Constant val)"; by (simp!);
    1.26  next;
    1.27    fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)";
    1.28 -    by (force simp add: exec_append);
    1.29 +    by (simp! add: exec_append);
    1.30  qed;
    1.31  
    1.32