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.

Larry Paulson

On 7 Apr 2006, at 15:39, Paqui Lucio wrote:

I am defining a new logic over Pure (indeed, I have almost achieve it). Now, I am trying to prove theorems using the rules (axioms) of my logic.
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 MHonArc.