# HG changeset patch
# User nipkow
# Date 989480930 -7200
# Node ID 6878bb02a7f90cb102367f73a745530e406d8b11
# Parent  d838df8795853dec12faff2452ec0a9cea0fe1b9
*** empty log message ***

diff -r d838df879585 -r 6878bb02a7f9 doc-src/TutorialI/Overview/Ind.thy
--- a/doc-src/TutorialI/Overview/Ind.thy	Thu May 10 09:41:45 2001 +0200
+++ b/doc-src/TutorialI/Overview/Ind.thy	Thu May 10 09:48:50 2001 +0200
@@ -88,8 +88,16 @@
   acc :: "('a \<times> 'a) set \<Rightarrow> 'a set"
 inductive "acc r"
 intros
-  "(\<forall>y. (x,y) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r"
+  "(\<forall>y. (y,x) \<in> r \<longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r"
 
+lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}"
+thm wfI
+apply(rule_tac A = "acc r" in wfI)
+ apply (blast elim:acc.elims)
+apply(simp(no_asm_use))
+thm acc.induct
+apply(erule acc.induct)
+by blast
 
 consts
   accs :: "('a \<times> 'a) set \<Rightarrow> 'a set"
diff -r d838df879585 -r 6878bb02a7f9 doc-src/TutorialI/Overview/RECDEF.thy
--- a/doc-src/TutorialI/Overview/RECDEF.thy	Thu May 10 09:41:45 2001 +0200
+++ b/doc-src/TutorialI/Overview/RECDEF.thy	Thu May 10 09:48:50 2001 +0200
@@ -48,6 +48,7 @@
 subsubsection{*Induction*}
 
 lemma "map f (sep(x,xs)) = sep(f x, map f xs)"
+thm sep.induct
 apply(induct_tac x xs rule: sep.induct)
 apply simp_all
 done