author wenzelm Thu, 24 Feb 2000 21:33:32 +0100 changeset 8297 f5fdb69ad4d2 parent 8296 c72122020380 child 8298 9b089bc07f69
simplified induct method;
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Feb 24 16:04:25 2000 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Thu Feb 24 21:33:32 2000 +0100
@@ -35,7 +35,7 @@
proof;
assume "t : tiling A" (is "_ : ?T");
thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t");
-  proof (induct t in set: tiling);
+  proof induct;
show "?P {}"; by simp;

fix a t;
@@ -168,7 +168,7 @@
assume b: "b < 2";
assume "d : domino";
thus ?thesis (is "?P d");
-  proof (induct d in set: domino);
+  proof induct;
from b; have b_cases: "b = 0 | b = 1"; by arith;
fix i j;
note [simp] = evnodd_empty evnodd_insert mod_Suc;
@@ -192,7 +192,7 @@
proof -;
assume "t : ?T";
thus "?F t";
-  proof (induct t in set: tiling);
+  proof induct;
show "?F {}"; by (rule Finites.emptyI);
fix a t; assume "?F t";
assume "a : domino"; hence "?F a"; by (rule domino_finite);
@@ -206,7 +206,7 @@
proof -;
assume "t : ?T";
thus "?P t";
-  proof (induct t in set: tiling);
+  proof induct;
show "?P {}"; by (simp add: evnodd_def);

fix a t;
--- a/src/HOL/Isar_examples/W_correct.thy	Thu Feb 24 16:04:25 2000 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy	Thu Feb 24 21:33:32 2000 +0100
@@ -45,7 +45,7 @@
proof -;
assume "a |- e :: t";
thus ?thesis (is "?P a e t");
-  proof (induct a e t in set: has_type);
+  proof induct;
fix a n;
assume "n < length (a::typ list)";
hence "n < length (map (\$ s) a)"; by simp;