equal
deleted
inserted
replaced
35 |
35 |
36 subsubsection {* Core syntax *} |
36 subsubsection {* Core syntax *} |
37 |
37 |
38 classes type |
38 classes type |
39 defaultsort type |
39 defaultsort type |
40 |
40 setup {* ObjectLogic.add_base_sort @{sort type} *} |
41 setup {* |
|
42 Typedecl.interpretation (fn a => fn thy => AxClass.axiomatize_arity |
|
43 (a, replicate (Sign.arity_number thy a) @{sort type}, @{sort type}) thy) |
|
44 *} |
|
45 |
41 |
46 arities |
42 arities |
47 "fun" :: (type, type) type |
43 "fun" :: (type, type) type |
48 itself :: (type) type |
44 itself :: (type) type |
49 |
45 |