--- a/src/HOL/Metis_Examples/Tarski.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy Mon Feb 08 21:28:27 2010 +0100
@@ -78,11 +78,9 @@
{S. S \<subseteq> pset cl &
(| pset = S, order = induced S (order cl) |): CompleteLattice }"
-syntax
- "@SL" :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
-
-translations
- "S <<= cl" == "S : sublattice `` {cl}"
+abbreviation
+ sublattice_syntax :: "['a set, 'a potype] => bool" ("_ <<= _" [51, 50] 50)
+ where "S <<= cl \<equiv> S : sublattice `` {cl}"
constdefs
dual :: "'a potype => 'a potype"