src/HOL/HOL.thy
changeset 21210 c17fd2df4e9e
parent 21179 99f546731724
child 21218 38013c3a77a2
     1.1 --- a/src/HOL/HOL.thy	Tue Nov 07 11:47:56 2006 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Nov 07 11:47:57 2006 +0100
     1.3 @@ -54,24 +54,24 @@
     1.4  
     1.5  subsubsection {* Additional concrete syntax *}
     1.6  
     1.7 -const_syntax (output)
     1.8 +notation (output)
     1.9    "op ="  (infix "=" 50)
    1.10  
    1.11  abbreviation
    1.12    not_equal     :: "['a, 'a] => bool"               (infixl "~=" 50)
    1.13    "x ~= y == ~ (x = y)"
    1.14  
    1.15 -const_syntax (output)
    1.16 +notation (output)
    1.17    not_equal  (infix "~=" 50)
    1.18  
    1.19 -const_syntax (xsymbols)
    1.20 +notation (xsymbols)
    1.21    Not  ("\<not> _" [40] 40)
    1.22    "op &"  (infixr "\<and>" 35)
    1.23    "op |"  (infixr "\<or>" 30)
    1.24    "op -->"  (infixr "\<longrightarrow>" 25)
    1.25    not_equal  (infix "\<noteq>" 50)
    1.26  
    1.27 -const_syntax (HTML output)
    1.28 +notation (HTML output)
    1.29    Not  ("\<not> _" [40] 40)
    1.30    "op &"  (infixr "\<and>" 35)
    1.31    "op |"  (infixr "\<or>" 30)
    1.32 @@ -81,7 +81,7 @@
    1.33    iff :: "[bool, bool] => bool"  (infixr "<->" 25)
    1.34    "A <-> B == A = B"
    1.35  
    1.36 -const_syntax (xsymbols)
    1.37 +notation (xsymbols)
    1.38    iff  (infixr "\<longleftrightarrow>" 25)
    1.39  
    1.40  
    1.41 @@ -215,12 +215,12 @@
    1.42  in map (tr' o Sign.const_syntax_name (the_context ())) ["HOL.one", "HOL.zero"] end;
    1.43  *} -- {* show types that are presumably too general *}
    1.44  
    1.45 -const_syntax
    1.46 +notation
    1.47    uminus  ("- _" [81] 80)
    1.48  
    1.49 -const_syntax (xsymbols)
    1.50 +notation (xsymbols)
    1.51    abs  ("\<bar>_\<bar>")
    1.52 -const_syntax (HTML output)
    1.53 +notation (HTML output)
    1.54    abs  ("\<bar>_\<bar>")
    1.55  
    1.56