Re: [isabelle] "by", "blast", etc without importing Main
Commands like "by" and tactics like "blast" are very different
things. If you have set up your logic correctly--and I admit that we
don't provide much documentation for people who set up new logics--
then the entire Isar proof language should be available to you.
However, tactics like "blast", "simp" and "auto" rely upon specific
inference rules being present in your logic. They need to be set up
separately for each logic. I'd be surprised if "blast" or "auto" can
be got working at all on top of a sequent-based logic, although a
very crude blast-like tactic is available.
On 7 Apr 2006, at 15:39, Paqui Lucio wrote:
I am defining a new logic over Pure (indeed, I have almost achieve
Now, I am trying to prove theorems using the rules (axioms) of my
However, I cannot use elemental commands like "by", or tactics like
"blast". It seems like I need Main (instead of Pure) to use them. Is
that true? In the positive case, what can I do to use this features
without using Main. The problem is that I use Sequents.thy which is
problematics to mix with Main.
This archive was generated by a fusion of
Pipermail (Mailman edition) and