154 proj (Bound 2) eqs n $ Bound 1 $ Bound 0, |
154 proj (Bound 2) eqs n $ Bound 1 $ Bound 0, |
155 foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) |
155 foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) |
156 ::map one_con cons)))); |
156 ::map one_con cons)))); |
157 in foldr1 mk_conj (mapn one_comp 0 eqs)end )); |
157 in foldr1 mk_conj (mapn one_comp 0 eqs)end )); |
158 fun add_one (thy,(dnam,axs,dfs)) = thy |
158 fun add_one (thy,(dnam,axs,dfs)) = thy |
159 |> Theory.add_path dnam |
159 |> Sign.add_path dnam |
160 |> add_defs_infer dfs |
160 |> add_defs_infer dfs |
161 |> add_axioms_infer axs |
161 |> add_axioms_infer axs |
162 |> Theory.parent_path; |
162 |> Sign.parent_path; |
163 val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); |
163 val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); |
164 in thy |> Theory.add_path comp_dnam |
164 in thy |> Sign.add_path comp_dnam |
165 |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) |
165 |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) |
166 |> Theory.parent_path |
166 |> Sign.parent_path |
167 end; |
167 end; |
168 |
168 |
169 end; (* local *) |
169 end; (* local *) |
170 end; (* struct *) |
170 end; (* struct *) |