Re: [isabelle] "by", "blast", etc without importing Main
I recall seeing blast_tac being used in the theory of ILL, also based on
Sequents, by Sara Kalvala and Valeria de Paiva. They have a paper
(ftp://ftp.dcs.warwick.ac.uk/people/Sara.Kalvala/lli.dvi) which talks
about this. This was done before Isar, so they don't have an Isar
bindings for blast but I guess you could make one for your logic so that
it can be used in the Isar scripts for your logic.
Lawrence Paulson wrote:
> 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