--- a/doc-src/TutorialI/Inductive/Advanced.thy Fri Nov 10 09:17:54 2000 +0100
+++ b/doc-src/TutorialI/Inductive/Advanced.thy Fri Nov 10 15:05:09 2000 +0100
@@ -1,5 +1,24 @@
(* ID: $Id$ *)
-theory Advanced = Main:
+theory Advanced = Even:
+
+text{* We completely forgot about "rule inversion", or whatever we may want
+to call it. Just as a demo I include the two forms that Markus has made available. First the one for binding the result to a name *}
+
+inductive_cases even_cases [elim!]:
+ "Suc(Suc n) \<in> even"
+
+thm even_cases;
+
+text{*and now the one for local usage:*}
+
+lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even";
+by(ind_cases "Suc(Suc n) \<in> even");
+
+text{*Both forms accept lists of strings.
+
+Hope you can find some more exciting examples, although these may do
+*}
+
datatype 'f "term" = Apply 'f "'f term list"