| changeset 31023 | d027411c9a38 |
| parent 30919 | dcf8a7a66bd1 |
| child 31227 | 0aa6afd229d3 |
| 31022:a438b4516dd3 | 31023:d027411c9a38 |
|---|---|
8 sig |
8 sig |
9 val add_axioms : bstring -> Domain_Library.eq list -> theory -> theory |
9 val add_axioms : bstring -> Domain_Library.eq list -> theory -> theory |
10 end; |
10 end; |
11 |
11 |
12 |
12 |
13 structure Domain_Axioms : DOMAIN_AXIOMS = |
13 structure Domain_Axioms :> DOMAIN_AXIOMS = |
14 struct |
14 struct |
15 |
15 |
16 local |
16 local |
17 |
17 |
18 open Domain_Library; |
18 open Domain_Library; |