# HG changeset patch
# User blanchet
# Date 1390238695 -3600
# Node ID 6b0fcbeebabab954039cb4099530b3c05634cdac
# Parent  b5c94200d081d4925d816441021c49d9b5d19f19
kill notations

diff -r b5c94200d081 -r 6b0fcbeebaba src/HOL/Main.thy
--- 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)