# HG changeset patch
# User wenzelm
# Date 951424412 -3600
# Node ID f5fdb69ad4d23edd00a58fae1c6f66ad262eb31b
# Parent  c721220203803b7674072d2c3ef959157f5c78a5
simplified induct method;

diff -r c72122020380 -r f5fdb69ad4d2 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- 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;
diff -r c72122020380 -r f5fdb69ad4d2 src/HOL/Isar_examples/W_correct.thy
--- 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;