| author | Walther Neuper <wneuper@ist.tugraz.at> |
| Fri, 22 Jan 2016 15:53:13 +0100 | |
| changeset 59209 | 907ce624bd20 |
| permissions | -rw-r--r-- |
1 theory Classy
2 imports Pure
3 keywords
4 "ML.class" :: thy_decl % "ML" and
5 "ML.instance" :: thy_decl % "ML" and
6 "ML.print_classes" :: diag
7 begin
9 ML_file "ml_types.ML"
10 ML_file "classy.ML"
12 setup \<open>Classy.setup\<close>
14 ML_file "pretty_class.ML"
16 ML.class pretty = \<open>'a pretty_class\<close>
18 ML.instance \<open>Pretty_Class.string\<close> :: pretty
19 ML.instance \<open>Pretty_Class.pretty\<close> :: pretty
20 ML.instance \<open>Pretty_Class.list\<close> :: pretty
22 end