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.
kill notations
authorblanchet
Mon, 20 Jan 2014 18:24:55 +0100
changeset 55057 6b0fcbeebaba
parent 55056 b5c94200d081
child 55058 4e700eb471d4
kill notations
src/HOL/Main.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Main.thy	Mon Jan 20 18:24:55 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 18:24:55 2014 +0100
@@ -17,7 +17,14 @@
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65) and
   Inf ("\<Sqinter>_" [900] 900) and
-  Sup ("\<Squnion>_" [900] 900)
+  Sup ("\<Squnion>_" [900] 900) and
+  ordLeq2 ("<=o") and
+  ordLeq3 ("\<le>o") and
+  ordLess2 ("<o") and
+  ordIso2 ("=o") and
+  csum (infixr "+c" 65) and
+  cprod (infixr "*c" 80) and
+  cexp (infixr "^c" 90)
 
 no_syntax (xsymbols)
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
isabelle