--- a/src/ZF/Induct/Comb.thy Tue Mar 02 23:56:13 2010 +0100
+++ b/src/ZF/Induct/Comb.thy Tue Mar 02 23:59:54 2010 +0100
@@ -23,6 +23,9 @@
| S
| app ("p \<in> comb", "q \<in> comb") (infixl "@@" 90)
+notation (xsymbols)
+ app (infixl "\<bullet>" 90)
+
text {*
Inductive definition of contractions, @{text "-1->"} and
(multi-step) reductions, @{text "--->"}.
@@ -39,9 +42,6 @@
contract_multi :: "[i,i] => o" (infixl "--->" 50)
where "p ---> q == <p,q> \<in> contract^*"
-syntax (xsymbols)
- "comb.app" :: "[i, i] => i" (infixl "\<bullet>" 90)
-
inductive
domains "contract" \<subseteq> "comb \<times> comb"
intros