| changeset 15816 | 4575c87dd25b |
| parent 13075 | d3e1d554cd6d |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/Induct/Comb.thy Fri Apr 22 17:32:03 2005 +0200 +++ b/src/HOL/Induct/Comb.thy Fri Apr 22 17:32:29 2005 +0200 @@ -39,6 +39,9 @@ "x -1-> y" == "(x,y) \<in> contract" "x ---> y" == "(x,y) \<in> contract^*" +syntax (xsymbols) + "op ##" :: "[comb,comb] => comb" (infixl "\<bullet>" 90) + inductive contract intros K: "K##x##y -1-> x"