equal
deleted
inserted
replaced
8 |
8 |
9 val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) -> |
9 val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) -> |
10 local_theory -> (term * thm) * local_theory |
10 local_theory -> (term * thm) * local_theory |
11 val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) -> |
11 val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) -> |
12 local_theory -> local_theory |
12 local_theory -> local_theory |
|
13 val diff: (typ * typ) -> (typ * typ) list -> (typ * typ) list |
13 end; |
14 end; |
14 |
15 |
15 structure Quotient_Def: QUOTIENT_DEF = |
16 structure Quotient_Def: QUOTIENT_DEF = |
16 struct |
17 struct |
17 |
18 |