equal
deleted
inserted
replaced
8 imports Ssum Sprod Up One Tr Fixrec Representable |
8 imports Ssum Sprod Up One Tr Fixrec Representable |
9 uses |
9 uses |
10 ("Tools/cont_consts.ML") |
10 ("Tools/cont_consts.ML") |
11 ("Tools/cont_proc.ML") |
11 ("Tools/cont_proc.ML") |
12 ("Tools/Domain/domain_constructors.ML") |
12 ("Tools/Domain/domain_constructors.ML") |
13 ("Tools/Domain/domain_library.ML") |
|
14 ("Tools/Domain/domain_axioms.ML") |
13 ("Tools/Domain/domain_axioms.ML") |
15 ("Tools/Domain/domain_theorems.ML") |
14 ("Tools/Domain/domain_theorems.ML") |
16 ("Tools/Domain/domain_extender.ML") |
15 ("Tools/Domain/domain_extender.ML") |
17 begin |
16 begin |
18 |
17 |
152 ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up |
151 ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up |
153 deflation_strict deflation_ID ID1 cfcomp2 |
152 deflation_strict deflation_ID ID1 cfcomp2 |
154 |
153 |
155 use "Tools/cont_consts.ML" |
154 use "Tools/cont_consts.ML" |
156 use "Tools/cont_proc.ML" |
155 use "Tools/cont_proc.ML" |
157 use "Tools/Domain/domain_library.ML" |
|
158 use "Tools/Domain/domain_axioms.ML" |
156 use "Tools/Domain/domain_axioms.ML" |
159 use "Tools/Domain/domain_constructors.ML" |
157 use "Tools/Domain/domain_constructors.ML" |
160 use "Tools/Domain/domain_theorems.ML" |
158 use "Tools/Domain/domain_theorems.ML" |
161 use "Tools/Domain/domain_extender.ML" |
159 use "Tools/Domain/domain_extender.ML" |
162 |
160 |