src/HOL/ROOT
Thu, 16 Jan 2014 16:33:19 +0100 blanchet moved 'Zorn' into 'Main', since it's a BNF dependency
Fri, 10 Jan 2014 11:47:10 +0100 traytel new codatatype example: stream processors
Mon, 18 Nov 2013 18:04:45 +0100 blanchet compile
Mon, 18 Nov 2013 18:04:44 +0100 blanchet split 'Cardinal_Arithmetic' 3-way
Mon, 18 Nov 2013 18:04:44 +0100 blanchet started three-way split of 'HOL-Cardinals'
Sat, 16 Nov 2013 18:34:11 +0100 wenzelm merged
Sat, 16 Nov 2013 16:57:09 +0100 wenzelm proper thy_load command 'boogie_file' -- avoid direct access to file-system;
Thu, 14 Nov 2013 13:03:09 +0100 haftmann explicit inclusion of data refinement theory into HOL-Library session
Wed, 23 Oct 2013 14:53:36 +0200 blanchet added 'primcorec' examples
Thu, 26 Sep 2013 22:34:43 +0200 wenzelm added Isabelle/ML example;
Tue, 24 Sep 2013 00:01:10 +0200 blanchet register codatatypes with Nitpick
Tue, 17 Sep 2013 14:10:33 +0200 kuncar include Int_Pow into Quotient_Examples; add end of the theory
Fri, 06 Sep 2013 10:56:40 +0200 noschinl added examples for Simps_Case_Conv
Fri, 30 Aug 2013 12:06:11 +0200 blanchet added example
Fri, 23 Aug 2013 12:40:55 +0200 wenzelm clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
Wed, 21 Aug 2013 09:25:40 +0200 blanchet renamed theory files to be closer to (new) command names
Wed, 24 Jul 2013 22:54:47 +0200 nipkow merged Def_Init_Sound_X into Def_Init_X
Tue, 23 Jul 2013 18:36:23 +0200 boehmes removed obsolete HOL-Boogie session;
Tue, 02 Jul 2013 14:48:01 +0200 wenzelm clarified Proofterm.proofs vs. Goal.skip_proofs;
Sun, 30 Jun 2013 12:30:02 +0200 wenzelm discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
Sun, 23 Jun 2013 16:47:45 +0200 wenzelm support for XML data representation of proof terms;
Thu, 20 Jun 2013 17:26:16 +0200 nipkow tuned theory name
Wed, 19 Jun 2013 10:14:50 +0200 nipkow more canonical name (2)
Mon, 10 Jun 2013 20:30:23 +0200 haftmann dropped relics of ancient binary numeral case study
Sat, 01 Jun 2013 12:02:41 +0200 nipkow tuned theory name
Fri, 31 May 2013 11:56:48 +0200 wenzelm make SML/NJ partially happy;
Fri, 31 May 2013 07:55:09 +0200 nipkow more VC -> VCG
Thu, 30 May 2013 20:09:49 +0200 bulwahn added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
Wed, 29 May 2013 23:11:21 +0200 wenzelm obsolete;
Fri, 05 Apr 2013 18:31:35 +0200 nipkow tuned document
Wed, 27 Mar 2013 21:07:10 +0100 wenzelm separate isatest with skip_proofs, to give some impression of performance without most of the proofs;
Wed, 27 Mar 2013 19:32:44 +0100 wenzelm tuned;
Wed, 27 Mar 2013 18:04:21 +0100 wenzelm allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
Wed, 27 Mar 2013 16:38:25 +0100 wenzelm more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Tue, 26 Mar 2013 20:37:32 +0100 wenzelm tuned session specification;
Mon, 25 Mar 2013 20:00:27 +0100 ballarin Discontinued theories src/HOL/Algebra/abstract and .../poly.
Wed, 13 Mar 2013 17:15:25 +0100 wenzelm proper formatting, to facilitate line-based diff;
Wed, 13 Mar 2013 17:13:22 +0100 wenzelm more uniform session descriptions, which show up in chapter index;
Tue, 12 Mar 2013 21:59:48 +0100 wenzelm refurbished some old README.html files as session descriptions, which show up in chapter index;
Mon, 11 Mar 2013 13:28:46 +0100 wenzelm support for 'chapter' specifications within session ROOT;
Sun, 24 Feb 2013 20:29:13 +0100 haftmann turned example into library for comparing growth of functions
Thu, 21 Feb 2013 18:21:40 +0100 wenzelm more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;
Fri, 15 Feb 2013 11:47:34 +0100 haftmann attempt to re-establish conventions which theories are loaded into the grand unified library theory;
Fri, 15 Feb 2013 11:47:33 +0100 haftmann systematic conversions between nat and nibble/char;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Thu, 14 Feb 2013 14:14:55 +0100 haftmann consolidation of library theories on product orders
Wed, 13 Feb 2013 13:38:52 +0100 haftmann tuned, particulary name
Sat, 19 Jan 2013 22:18:35 +0100 wenzelm afford parallel proof terms;
Sun, 13 Jan 2013 22:05:47 +0100 wenzelm hardwired document_variants, to prevent HOL-IMP's \snip choking on macros from isabellestags.sty;
Sat, 12 Jan 2013 14:56:57 +0100 wenzelm populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
Fri, 11 Jan 2013 14:33:44 +0100 wenzelm discontinued HOL side-entry sessions -- may be configured in $ISABELLE_HOME_USER/ROOT instead;
Wed, 02 Jan 2013 09:31:25 +0100 blanchet actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
Wed, 02 Jan 2013 09:13:50 +0100 blanchet added missing certificate file to "ROOT"
Sat, 29 Dec 2012 17:18:01 +0100 nipkow new theory Library/Finite_Lattice
Sun, 16 Dec 2012 21:27:23 +0100 wenzelm HOL-Quickcheck_Benchmark works without timeout (NB: isatest imposes global timeout already);
Sun, 16 Dec 2012 18:12:18 +0100 bulwahn reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again
Thu, 13 Dec 2012 15:36:08 +0100 traytel renamed theory
Tue, 11 Dec 2012 22:19:39 +0100 wenzelm disable Find_Unused_Assms_Examples for now, to recover isatest sanity;
Tue, 04 Dec 2012 18:00:40 +0100 hoelzl remove SMT proofs in Multivariate_Analysis
Fri, 23 Nov 2012 22:16:52 +0100 wenzelm timeout in proper place (HOL-Quickcheck_Examples approx. 1min, HOL-Quickcheck_Benchmark approx. 1h);
less more (0) -100 -60 tip