equal
deleted
inserted
replaced
23 |
23 |
24 val domaindef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string |
24 val domaindef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string |
25 * (binding * binding) option -> theory -> theory |
25 * (binding * binding) option -> theory -> theory |
26 end |
26 end |
27 |
27 |
28 structure Domaindef :> DOMAINDEF = |
28 structure Domaindef : DOMAINDEF = |
29 struct |
29 struct |
30 |
30 |
31 open HOLCF_Library |
31 open HOLCF_Library |
32 |
32 |
33 infixr 6 ->> |
33 infixr 6 ->> |