[isabelle-dev] smt2

Makarius makarius at sketis.net
Fri Mar 14 16:39:37 CET 2014

On Fri, 14 Mar 2014, Andreas Lochbihler wrote:

> IIRC, the AFP policy is (was?) that all entries that import at least one 
> theory from HOL-Library are based on HOL-Library.

I can't speak for the AFP editors, but that might be just some 
old-fashioned custom.  In general it does not even work out, since the 
session images structure is just a tree, without the possibility of merge 

I have recently started to rethink the way theory imports from other 
sessions are specified, which would remove any coincidence on how the 
image tree was formed, oddities like "../Foo/Bar" vs just Bar, and 
oddities about fluctuating options [document = false].  As usual such 
reforms are encumbered by having to think thrice: for batch build, PIDE, 
Proof General.  Getting rid of the latter would speed the process.

I'd like to see a situation where one can just fire up the Prover IDE and 
edit any of the AFP theories without thinking about accidental session 


More information about the isabelle-dev mailing list