- Now imports Fun rather than Orderings
- Moved "Set as lattice" section behind "Fun as lattice" section, since
sets are just functions.
- The instantiations
instantiation set :: (type) distrib_lattice
instantiation set :: (type) complete_lattice
are no longer needed, and the former definitions inf_set_eq, sup_set_eq,
Inf_set_def, and Sup_set_def can now be derived from abstract properties
of sup, inf, etc.
header {* \section{Concrete Syntax} *}
theory Quote_Antiquote imports Main begin
syntax
"_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(\<guillemotleft>_\<guillemotright>)" [0] 1000)
"_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000)
"_Assert" :: "'a \<Rightarrow> 'a set" ("(.{_}.)" [0] 1000)
syntax (xsymbols)
"_Assert" :: "'a \<Rightarrow> 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)
translations
".{b}." \<rightharpoonup> "Collect \<guillemotleft>b\<guillemotright>"
parse_translation {*
let
fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
| quote_tr ts = raise TERM ("quote_tr", ts);
in [("_quote", quote_tr)] end
*}
end