src/HOL/Library/OptionalSugar.thy
changeset 61955 e96292f32c3c
parent 61645 ae5e55d03e45
child 63935 aa1fe1103ab8
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  
     1.5  (* sorts as intersections *)
     1.6  
     1.7 -syntax (xsymbols output)
     1.8 +syntax (output)
     1.9    "_topsort" :: "sort"  ("\<top>" 1000)
    1.10    "_sort" :: "classes => sort"  ("'(_')" 1000)
    1.11    "_classes" :: "id => classes => classes"  ("_ \<inter> _" 1000)