[isabelle-dev] smt2

[Makarius]

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 
nodes.

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 
images.


 	Makarius