[isabelle-dev] HOL/Plain.thy [was: Purpose of additional HOL images]

[Florian Haftmann]

> Experts on HOL's structure are welcome to reconsider it eventually.  For
> the release we should not open that can, though.

See now http://isabelle.in.tum.de/repos/isabelle/rev/da97167e03f7.

There is no observable effect on runtime behaviour:

> on lxbroy10 with Plain.thy
> 	Running HOL ...
> 	Finished HOL (0:02:10 elapsed time, 0:06:04 cpu time, factor 2.80)
> 	Running HOL-Proofs ...
> 	Finished HOL-Proofs (0:02:01 elapsed time, 0:09:58 cpu time, factor 4.94)
> on lxbroy10 without Plain.thy
> 	Running HOL ...
> 	Finished HOL (0:02:13 elapsed time, 0:06:03 cpu time, factor 2.72)
> 	Running HOL-Proofs ...
> 	Finished HOL-Proofs (0:02:02 elapsed time, 0:09:56 cpu time, factor 4.88)

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130214/b468adb6/attachment.asc>