# HG changeset patch
# User wenzelm
# Date 951252602 -3600
# Node ID 188e2924433e5a034780acde9bb4c29021a6e02d
# Parent  259073d16f84a2a7fe19302b78359857748c0ecc
tuned "induct" syntax;

diff -r 259073d16f84 -r 188e2924433e src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Feb 22 21:49:34 2000 +0100
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Feb 22 21:50:02 2000 +0100
@@ -114,12 +114,12 @@
 lemma exec_append:
   "ALL stack. exec (xs @ ys) stack env =
     exec ys (exec xs stack env) env" (is "?P xs");
-proof (induct ?P xs type: list);
+proof (induct ?P xs in type: list);
   show "?P []"; by simp;
 
   fix x xs; assume "?P xs";
   show "?P (x # xs)" (is "?Q x");
-  proof (induct ?Q x type: instr);
+  proof (induct ?Q x in type: instr);
     show "!!val. ?Q (Const val)"; by (simp!);
     show "!!adr. ?Q (Load adr)"; by (simp!);
     show "!!fun. ?Q (Apply fun)"; by (simp!);
@@ -130,7 +130,7 @@
 proof -;
   have "ALL stack. exec (compile e) stack env =
     eval e env # stack" (is "?P e");
-  proof (induct ?P e type: expr);
+  proof (induct ?P e in type: expr);
     show "!!adr. ?P (Variable adr)"; by simp;
     show "!!val. ?P (Constant val)"; by simp;
     show "!!fun e1 e2. (?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2))";
diff -r 259073d16f84 -r 188e2924433e src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Tue Feb 22 21:49:34 2000 +0100
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Tue Feb 22 21:50:02 2000 +0100
@@ -35,7 +35,7 @@
 lemmas [simp] = fib.rules;
 
 lemma [simp]: "0 < fib (Suc n)";
-  by (induct n function: fib) (simp+);
+  by (induct n in function: fib) (simp+);
 
 
 text {* Alternative induction rule. *};
diff -r 259073d16f84 -r 188e2924433e src/HOL/Isar_examples/MultisetOrder.thy
--- a/src/HOL/Isar_examples/MultisetOrder.thy	Tue Feb 22 21:49:34 2000 +0100
+++ b/src/HOL/Isar_examples/MultisetOrder.thy	Tue Feb 22 21:50:02 2000 +0100
@@ -22,8 +22,8 @@
     (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"
   (concl is "?case1 (mult1 r) | ?case2");
 proof (unfold mult1_def);
-  let ?r = "\<lambda>K a. ALL b. elem K b --> (b, a) : r";
-  let ?R = "\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
+  let ?r = "\\<lambda>K a. ALL b. elem K b --> (b, a) : r";
+  let ?R = "\\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
   let ?case1 = "?case1 {(N, M). ?R N M}";
 
   assume "(N, M0 + {#a#}) : {(N, M). ?R N M}";
@@ -84,7 +84,7 @@
 	assume N: "N = M0 + K";
 	assume "ALL b. elem K b --> (b, a) : r";
 	have "?this --> M0 + K : ?W" (is "?P K");
-	proof (induct K rule: multiset_induct);
+	proof (induct K in rule: multiset_induct);
 	  from M0; have "M0 + {#} : ?W"; by simp;
 	  thus "?P {#}"; ..;
 
@@ -109,7 +109,7 @@
   assume wf: "wf r";
   fix M;
   show "M : ?W";
-  proof (induct M rule: multiset_induct);
+  proof (induct M in rule: multiset_induct);
     show "{#} : ?W";
     proof (rule accI);
       fix b; assume "(b, {#}) : ?R";
diff -r 259073d16f84 -r 188e2924433e src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Feb 22 21:49:34 2000 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Feb 22 21:50:02 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 set: tiling);
+  proof (induct t in set: tiling);
     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 set: domino);
+  proof (induct d in set: domino);
     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 set: tiling);
+  proof (induct t in set: tiling);
     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 set: tiling);
+  proof (induct t in set: tiling);
     show "?P {}"; by (simp add: evnodd_def);
 
     fix a t;
diff -r 259073d16f84 -r 188e2924433e src/HOL/Isar_examples/W_correct.thy
--- a/src/HOL/Isar_examples/W_correct.thy	Tue Feb 22 21:49:34 2000 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy	Tue Feb 22 21:50:02 2000 +0100
@@ -45,7 +45,7 @@
 proof -;
   assume "a |- e :: t";
   thus ?thesis (is "?P a e t");
-  proof (rule has_type.induct);     (* FIXME induct method *)
+  proof (induct a e t in set: has_type);
     fix a n;
     assume "n < length (a::typ list)";
     hence "n < length (map ($ s) a)"; by simp;