src/HOL/Proofs/Extraction/Warshall.thy
Thu, 02 Jul 2020 12:10:58 +0000 haftmann extraction of equations x = t from premises beneath meta-all
Tue, 02 Jan 2018 16:40:54 +0100 blanchet updated dependencies + compile
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Fri, 01 Jul 2016 16:52:35 +0200 wenzelm misc tuning and modernization;
Wed, 30 Dec 2015 18:25:39 +0100 wenzelm isabelle update_cartouches -c -t;
Sat, 27 Jun 2015 00:10:24 +0200 wenzelm premises in 'show' are treated like 'assume';
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Tue, 07 Oct 2014 23:12:08 +0200 wenzelm more antiquotations;
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Tue, 09 Sep 2014 20:51:36 +0200 blanchet removed 'datatype_compat's that are no longer needed
Tue, 09 Sep 2014 20:51:36 +0200 blanchet ported HOL-Proofs-Extraction to new datatypes
Mon, 25 Feb 2013 12:17:50 +0100 wenzelm prefer stateless 'ML_val' for tests;
Mon, 06 Sep 2010 14:18:16 +0200 wenzelm more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
less more (0) tip