src/ZF/Induct/Comb.thy
changeset 35427 ad039d29e01c
parent 35068 544867142ea4
child 46822 95f1e700b712
     1.1 --- a/src/ZF/Induct/Comb.thy	Tue Mar 02 23:56:13 2010 +0100
     1.2 +++ b/src/ZF/Induct/Comb.thy	Tue Mar 02 23:59:54 2010 +0100
     1.3 @@ -23,6 +23,9 @@
     1.4    | S
     1.5    | app ("p \<in> comb", "q \<in> comb")    (infixl "@@" 90)
     1.6  
     1.7 +notation (xsymbols)
     1.8 +  app  (infixl "\<bullet>" 90)
     1.9 +
    1.10  text {*
    1.11    Inductive definition of contractions, @{text "-1->"} and
    1.12    (multi-step) reductions, @{text "--->"}.
    1.13 @@ -39,9 +42,6 @@
    1.14    contract_multi :: "[i,i] => o"    (infixl "--->" 50)
    1.15    where "p ---> q == <p,q> \<in> contract^*"
    1.16  
    1.17 -syntax (xsymbols)
    1.18 -  "comb.app"    :: "[i, i] => i"             (infixl "\<bullet>" 90)
    1.19 -
    1.20  inductive
    1.21    domains "contract" \<subseteq> "comb \<times> comb"
    1.22    intros