equal
deleted
inserted
replaced
94 OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl |
94 OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl |
95 (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)) |
95 (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)) |
96 >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd)); |
96 >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd)); |
97 |
97 |
98 val _ = |
98 val _ = |
99 OuterSyntax.local_theory "defaultsort" "declare default sort for explicit type variables" |
99 OuterSyntax.local_theory "default_sort" "declare default sort for explicit type variables" |
100 K.thy_decl |
100 K.thy_decl |
101 (P.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); |
101 (P.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); |
102 |
102 |
103 |
103 |
104 (* types *) |
104 (* types *) |