equal
deleted
inserted
replaced
2 Author: David von Oheimb |
2 Author: David von Oheimb |
3 |
3 |
4 Syntax generator for domain command. |
4 Syntax generator for domain command. |
5 *) |
5 *) |
6 |
6 |
7 structure Domain_Axioms = struct |
7 signature DOMAIN_AXIOMS = |
|
8 sig |
|
9 val add_axioms : bstring -> Domain_Library.eq list -> theory -> theory |
|
10 end; |
|
11 |
|
12 |
|
13 structure Domain_Axioms : DOMAIN_AXIOMS = |
|
14 struct |
8 |
15 |
9 local |
16 local |
10 |
17 |
11 open Domain_Library; |
18 open Domain_Library; |
12 infixr 0 ===>;infixr 0 ==>;infix 0 == ; |
19 infixr 0 ===>;infixr 0 ==>;infix 0 == ; |
137 val ms = map qualify con_names ~~ map qualify mat_names; |
144 val ms = map qualify con_names ~~ map qualify mat_names; |
138 in FixrecPackage.add_matchers ms thy end; |
145 in FixrecPackage.add_matchers ms thy end; |
139 |
146 |
140 in (* local *) |
147 in (* local *) |
141 |
148 |
142 fun add_axioms (comp_dnam, eqs : eq list) thy' = let |
149 fun add_axioms comp_dnam (eqs : eq list) thy' = let |
143 val comp_dname = Sign.full_bname thy' comp_dnam; |
150 val comp_dname = Sign.full_bname thy' comp_dnam; |
144 val dnames = map (fst o fst) eqs; |
151 val dnames = map (fst o fst) eqs; |
145 val x_name = idx_name dnames "x"; |
152 val x_name = idx_name dnames "x"; |
146 fun copy_app dname = %%:(dname^"_copy")`Bound 0; |
153 fun copy_app dname = %%:(dname^"_copy")`Bound 0; |
147 val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == |
154 val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == |