GitLab

When cloning a theory, the behavior is to keep axioms as axioms, unless the user explicitly put a with lemma foo clause. This approach is error-prone, as it will cause (possibly inconsistent) facts to never get any proof obligation, due to the user forgetting about them at clone time. I suggest that the default behavior be changed so that any cloned axiom produces a proof obligation, unless the user explicitly put a with axiom foo clause. For the sake of conciseness, there should be a special syntax (e.g. with axiom *) to skip over all the remaining cloned axioms. Another possibility would be to not turn cloned axioms into lemmas if none of their symbols got instantiated at clone time.