--- a/src/ZF/Induct/Comb.thy Wed Apr 27 16:40:27 2005 +0200
+++ b/src/ZF/Induct/Comb.thy Wed Apr 27 16:41:03 2005 +0200
@@ -39,7 +39,7 @@
"p ---> q" == "<p,q> \<in> contract^*"
syntax (xsymbols)
- "app" :: "[i, i] => i" (infixl "\<bullet>" 90)
+ "comb.app" :: "[i, i] => i" (infixl "\<bullet>" 90)
inductive
domains "contract" \<subseteq> "comb \<times> comb"
@@ -158,8 +158,6 @@
and S_contractE [elim!]: "S -1-> r"
and Ap_contractE [elim!]: "p\<bullet>q -1-> r"
-declare contract.Ap1 [intro] contract.Ap2 [intro]
-
lemma I_contract_E: "I -1-> r ==> P"
by (auto simp add: I_def)