# HG changeset patch
# User wenzelm
# Date 934985127 -7200
# Node ID a494a78fea3927b6ec3a31e77a46c44a58723bee
# Parent  d3ed595dd772d52d43b99607546e4e02d08f1da1
tuned;

diff -r d3ed595dd772 -r a494a78fea39 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Wed Aug 18 16:04:00 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Wed Aug 18 16:05:27 1999 +0200
@@ -108,23 +108,23 @@
   assume "??P xs";
   show "??P (x # xs)" (is "??Q x");
   proof (induct ??Q x type: instr);
-    fix val; show "??Q (Const val)"; by brute_force;
+    fix val; show "??Q (Const val)"; by force;
   next;
-    fix adr; show "??Q (Load adr)"; by brute_force;
+    fix adr; show "??Q (Load adr)"; by force;
   next;
-    fix fun; show "??Q (Apply fun)"; by brute_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 brute_force;
+  fix adr; show "??P (Variable adr)"; by force;
 next;
-  fix val; show "??P (Constant val)"; by brute_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)";
-    by (brute_force simp add: exec_append);
+    by (force simp add: exec_append);
 qed;
 
 
diff -r d3ed595dd772 -r a494a78fea39 src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Wed Aug 18 16:04:00 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Wed Aug 18 16:05:27 1999 +0200
@@ -9,7 +9,6 @@
 theory KnasterTarski = Main:;
 
 text {*
-
  According to the book ``Introduction to Lattices and Order'' (by
  B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski
  fixpoint theorem is as follows (pages 93--94).  Note that we have