[isabelle] "by", "blast", etc without importing Main
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.
Facultad de Informática
Universidad del País Vasco
This archive was generated by a fusion of
Pipermail (Mailman edition) and