1.1 --- a/src/HOL/Metis_Examples/Tarski.thy	Tue Oct 20 19:52:04 2009 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Tarski.thy	Mon Feb 08 21:28:27 2010 +0100
     1.3 @@ -78,11 +78,9 @@
     1.4            {S. S \<subseteq> pset cl &
     1.5             (| pset = S, order = induced S (order cl) |): CompleteLattice }"
     1.6  
     1.7 -syntax
     1.8 -  "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
     1.9 -
    1.10 -translations
    1.11 -  "S <<= cl" == "S : sublattice `` {cl}"
    1.12 +abbreviation
    1.13 +  sublattice_syntax :: "['a set, 'a potype] => bool" ("_ <<= _" [51, 50] 50)
    1.14 +  where "S <<= cl \<equiv> S : sublattice `` {cl}"
    1.15  
    1.16  constdefs
    1.17    dual :: "'a potype => 'a potype"