1.1 --- a/src/ZF/Induct/Comb.thy	Wed Apr 27 16:40:27 2005 +0200
     1.2 +++ b/src/ZF/Induct/Comb.thy	Wed Apr 27 16:41:03 2005 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4    "p ---> q" == "<p,q> \<in> contract^*"
     1.5  
     1.6  syntax (xsymbols)
     1.7 -  "app"    :: "[i, i] => i"    	     (infixl "\<bullet>" 90)
     1.8 +  "comb.app"    :: "[i, i] => i"    	     (infixl "\<bullet>" 90)
     1.9  
    1.10  inductive
    1.11    domains "contract" \<subseteq> "comb \<times> comb"
    1.12 @@ -158,8 +158,6 @@
    1.13    and S_contractE [elim!]: "S -1-> r"
    1.14    and Ap_contractE [elim!]: "p\<bullet>q -1-> r"
    1.15  
    1.16 -declare contract.Ap1 [intro] contract.Ap2 [intro]
    1.17 -
    1.18  lemma I_contract_E: "I -1-> r ==> P"
    1.19    by (auto simp add: I_def)
    1.20