Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
x-symbol syntax
authorpaulson
Fri, 22 Apr 2005 17:32:29 +0200
changeset 15816 4575c87dd25b
parent 15815 62854cac5410
child 15817 f79b673da664
x-symbol syntax
src/HOL/Induct/Comb.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle