# HG changeset patch
# User wenzelm
# Date 937927855 -7200
# Node ID bfa85f42962947cf936096c1586466136b5c4e7d
# Parent  90455fa8cebe91ab988a079e09e7917ea7b6da79
accomodate refined facts handling;
tuned;

diff -r 90455fa8cebe -r bfa85f429629 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Sep 21 17:30:11 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Sep 21 17:30:55 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 force;
+    fix val; show "?Q (Const val)"; by (simp!);
   next;
-    fix adr; show "?Q (Load adr)"; by force;
+    fix adr; show "?Q (Load adr)"; by (simp!);
   next;
-    fix fun; show "?Q (Apply fun)"; by force;
+    fix fun; show "?Q (Apply fun)"; by (simp!);
   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;
+  fix adr; show "?P (Variable adr)"; by (simp!);
 next;
-  fix val; show "?P (Constant val)"; by force;
+  fix val; show "?P (Constant val)"; by (simp!);
 next;
   fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)";
-    by (force simp add: exec_append);
+    by (simp! add: exec_append);
 qed;
 
 
diff -r 90455fa8cebe -r bfa85f429629 src/HOL/Isar_examples/MultisetOrder.thy
--- a/src/HOL/Isar_examples/MultisetOrder.thy	Tue Sep 21 17:30:11 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy	Tue Sep 21 17:30:55 1999 +0200
@@ -40,7 +40,7 @@
       with N; have n: "N = K' + K + {#a#}"; by (simp add: union_ac);
 
       assume "M0 = K' + {#a'#}";
-      with r; have "?R (K' + K) M0"; by simp blast;
+      with r; have "?R (K' + K) M0"; by blast;
       with n; have ?case1; by simp; thus ?thesis; ..;
     qed;
   qed;
diff -r 90455fa8cebe -r bfa85f429629 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 21 17:30:11 1999 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 21 17:30:55 1999 +0200
@@ -38,8 +38,8 @@
     show "?P (a Un t)";
     proof (intro impI);
       assume "u : ?T" "(a Un t) Int u = {}";
-      have hyp: "t Un u: ?T"; by blast;
-      have "a <= - (t Un u)"; by blast;
+      have hyp: "t Un u: ?T"; by (blast!);
+      have "a <= - (t Un u)"; by (blast!);
       with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un);
       also; have "a Un (t Un u) = (a Un t) Un u"; by (simp only: Un_assoc);
       finally; show "... : ?T"; .;
@@ -153,11 +153,11 @@
 
 lemma domino_singleton: "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}";
 proof -;
-  assume "b < 2";
+  assume b: "b < 2";
   assume "d : domino";
   thus ?thesis (is "?P d");
   proof (induct d set: domino);
-    have b_cases: "b = 0 | b = 1"; by arith;
+    from b; have b_cases: "b = 0 | b = 1"; by arith;
     fix i j;
     note [simp] = evnodd_empty evnodd_insert mod_Suc;
     from b_cases; show "?P {(i, j), (i, j + 1)}"; by rule auto;
@@ -208,13 +208,13 @@
       thus "?thesis b";
       proof (elim exE);
 	have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un);
-	also; fix i j; assume "?e a b = {(i, j)}";
+	also; fix i j; assume e: "?e a b = {(i, j)}";
 	also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp;
 	also; have "card ... = Suc (card (?e t b))";
 	proof (rule card_insert_disjoint);
 	  show "finite (?e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
-	  have "(i, j) : ?e a b"; by asm_simp;
-	  thus "(i, j) ~: ?e t b"; by (force dest: evnoddD);
+	  have "(i, j) : ?e a b"; by (simp!);
+	  thus "(i, j) ~: ?e t b"; by (force! dest: evnoddD);
 	qed;
 	finally; show ?thesis; .;
       qed;