--- 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"