diff -r 3c82b641b642 -r 094b76968484 doc-src/TutorialI/Inductive/Advanced.thy
--- a/doc-src/TutorialI/Inductive/Advanced.thy	Wed Feb 21 12:07:00 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Advanced.thy	Wed Feb 21 12:57:55 2001 +0100
@@ -56,7 +56,7 @@
 \rulename{gterm_Apply_elim}
 *}
 
-lemma gterms_IntI [rule_format]:
+lemma gterms_IntI [rule_format, intro!]:
      "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
 apply (erule gterms.induct)
 txt{*
@@ -73,10 +73,7 @@
 
 lemma gterms_Int_eq [simp]:
      "gterms (F\<inter>G) = gterms F \<inter> gterms G"
-apply (rule equalityI)
-apply (blast intro!: mono_Int monoI gterms_mono)
-apply (blast intro!: gterms_IntI)
-done
+by (blast intro!: mono_Int monoI gterms_mono)
 
 
 consts integer_arity :: "integer_op \<Rightarrow> nat"