equal
deleted
inserted
replaced
12 open Domain_Library; |
12 open Domain_Library; |
13 infixr 0 ===>;infixr 0 ==>;infix 0 == ; |
13 infixr 0 ===>;infixr 0 ==>;infix 0 == ; |
14 infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; |
14 infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; |
15 infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; |
15 infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; |
16 |
16 |
17 fun infer_types thy' = map (inferT_axm (sign_of thy')); |
17 fun infer_types thy' = map (inferT_axm thy'); |
18 |
18 |
19 fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)= |
19 fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)= |
20 let |
20 let |
21 |
21 |
22 (* ----- axioms and definitions concerning the isomorphism ------------------ *) |
22 (* ----- axioms and definitions concerning the isomorphism ------------------ *) |
118 fun add_defs_infer defs thy = add_defs_i (infer_types thy defs) thy; |
118 fun add_defs_infer defs thy = add_defs_i (infer_types thy defs) thy; |
119 |
119 |
120 in (* local *) |
120 in (* local *) |
121 |
121 |
122 fun add_axioms (comp_dnam, eqs : eq list) thy' = let |
122 fun add_axioms (comp_dnam, eqs : eq list) thy' = let |
123 val comp_dname = Sign.full_name (sign_of thy') comp_dnam; |
123 val comp_dname = Sign.full_name thy' comp_dnam; |
124 val dnames = map (fst o fst) eqs; |
124 val dnames = map (fst o fst) eqs; |
125 val x_name = idx_name dnames "x"; |
125 val x_name = idx_name dnames "x"; |
126 fun copy_app dname = %%:(dname^"_copy")`Bound 0; |
126 fun copy_app dname = %%:(dname^"_copy")`Bound 0; |
127 val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == |
127 val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == |
128 /\"f"(foldr1 cpair (map copy_app dnames))); |
128 /\"f"(foldr1 cpair (map copy_app dnames))); |