libisabelle-protocol/isabelle/2015/lib/classy/Classy.thy
changeset 59209 907ce624bd20
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/libisabelle-protocol/isabelle/2015/lib/classy/Classy.thy	Fri Jan 22 15:53:13 2016 +0100
     1.3 @@ -0,0 +1,22 @@
     1.4 +theory Classy
     1.5 +imports Pure
     1.6 +keywords
     1.7 +  "ML.class" :: thy_decl % "ML" and
     1.8 +  "ML.instance" :: thy_decl % "ML" and
     1.9 +  "ML.print_classes" :: diag
    1.10 +begin
    1.11 +
    1.12 +ML_file "ml_types.ML"
    1.13 +ML_file "classy.ML"
    1.14 +
    1.15 +setup \<open>Classy.setup\<close>
    1.16 +
    1.17 +ML_file "pretty_class.ML"
    1.18 +
    1.19 +ML.class pretty = \<open>'a pretty_class\<close>
    1.20 +
    1.21 +ML.instance \<open>Pretty_Class.string\<close> :: pretty
    1.22 +ML.instance \<open>Pretty_Class.pretty\<close> :: pretty
    1.23 +ML.instance \<open>Pretty_Class.list\<close> :: pretty
    1.24 +
    1.25 +end
    1.26 \ No newline at end of file