src/HOL/ROOT
Tue, 22 Sep 2015 08:38:25 +0200 nipkow added red black trees
Mon, 21 Sep 2015 14:44:32 +0200 nipkow New subdirectory for functional data structures
Thu, 10 Sep 2015 16:42:01 +0200 wenzelm HOL-Proofs is slow;
Wed, 09 Sep 2015 17:07:44 +0200 Andreas Lochbihler reactivate examples with predicate compiler and quickcheck
Wed, 12 Aug 2015 20:46:33 +0200 traytel actually process lift_bnf regression suite
Tue, 28 Jul 2015 16:16:13 +0100 paulson the Cauchy integral theorem and related material
Mon, 27 Jul 2015 22:44:02 +0200 haftmann formal class for factorial (semi)rings
Sat, 18 Jul 2015 20:37:16 +0200 wenzelm reactivated dead code;
Fri, 12 Jun 2015 10:33:02 +0200 bulwahn add examples from Freek's top 100 theorems (thms 30, 73, 77)
Sun, 14 Jun 2015 16:18:00 +0200 wenzelm more examples;
Sat, 13 Jun 2015 13:18:37 +0200 wenzelm more examples;
Mon, 01 Jun 2015 15:39:53 +0200 wenzelm discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;
Sat, 02 May 2015 13:58:06 +0200 kuncar add testing file for code_dt extension of lifting
Fri, 17 Apr 2015 17:49:19 +0200 wenzelm added Eisbach, using version 3752768caa17 of its Bitbucket repository;
Sat, 11 Apr 2015 12:24:51 +0200 wenzelm make SML/NJ more happy;
Thu, 09 Apr 2015 22:53:26 +0200 wenzelm make SML/NJ more happy;
Wed, 08 Apr 2015 20:41:56 +0200 wenzelm proper test for session HOL-Library;
Fri, 03 Apr 2015 21:25:55 +0200 wenzelm rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
Wed, 01 Apr 2015 22:40:41 +0200 wenzelm merged
Wed, 01 Apr 2015 18:22:55 +0200 wenzelm clarified "main" group, e.g. relevant for Isabelle/jEdit menu;
Wed, 01 Apr 2015 15:47:55 +0100 paulson John Harrison's example: a 32-bit approximation to pi. SLOW
Wed, 25 Mar 2015 13:31:47 +0100 wenzelm HOL-SPARK .prv files are subject to system option spark_prv;
Mon, 23 Mar 2015 08:45:54 +0100 nipkow BT subsumed by Library/Tree
Wed, 18 Mar 2015 21:40:21 +0100 traytel bounded powerset
Wed, 18 Mar 2015 14:28:40 +0000 paulson Merge
Wed, 18 Mar 2015 14:13:27 +0000 paulson Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
Wed, 18 Mar 2015 13:51:33 +0100 noschinl added proof method rewrite
Tue, 10 Mar 2015 15:20:40 +0000 paulson Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
Tue, 10 Feb 2015 23:02:39 +0100 wenzelm check unused theory;
Sun, 25 Jan 2015 22:11:06 +0100 wenzelm discontinued obsolete option "document_graph";
Sun, 28 Dec 2014 15:42:34 +1100 kleing 3 old example lemmas by Amine listed in the top 100 theorems
Sat, 20 Dec 2014 00:05:20 +0100 wenzelm afford full test, with slightly improved scheduling order;
Wed, 17 Dec 2014 16:10:30 +0100 hoelzl unfortunately, there is no general function space in the measurable spaces
Thu, 04 Dec 2014 20:56:38 +0100 wenzelm more examples;
Fri, 14 Nov 2014 21:36:50 +0100 wenzelm no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
Fri, 31 Oct 2014 18:56:59 +0100 wenzelm discontinued pointless option: timing is always on (overall theory only);
Fri, 31 Oct 2014 11:18:17 +0100 wenzelm discontinued Proof General;
Fri, 10 Oct 2014 18:23:59 +0200 nipkow New example Bubblesort
Wed, 08 Oct 2014 11:09:17 +0200 wenzelm simplified "sos" method;
Wed, 08 Oct 2014 09:09:12 +0200 Andreas Lochbihler move Code_Test to HOL/Library;
Tue, 07 Oct 2014 23:29:43 +0200 wenzelm more bibtex entries;
Wed, 24 Sep 2014 17:33:53 +0200 blanchet made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow
Mon, 22 Sep 2014 21:45:59 +0200 wenzelm clarified timeout for isatest;
Mon, 22 Sep 2014 16:28:24 +0200 wenzelm examples for local CSDP executable;
Mon, 22 Sep 2014 16:15:29 +0200 wenzelm clarified SOS tool setup vs. examples;
Mon, 22 Sep 2014 10:18:41 +0200 wenzelm clarified ISABELLE_POLYML;
Sun, 21 Sep 2014 20:22:12 +0200 wenzelm renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
Fri, 19 Sep 2014 10:00:34 +0200 traytel regression tests for n2m
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, 18 Sep 2014 16:47:40 +0200 blanchet increased 'HOL-Proofs' timeout
Thu, 18 Sep 2014 00:03:46 +0200 blanchet renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
Tue, 16 Sep 2014 19:23:37 +0200 blanchet took out 'old_datatype' examples -- those just cause timeouts in Isatests
Fri, 12 Sep 2014 17:51:31 +0200 blanchet enabled 'Sudoku' only with 'ISABELLE_FULL_TEST' -- Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
Fri, 12 Sep 2014 16:42:36 +0200 blanchet run larger nominal examples only 'ISABELLE_FULL_TEST'
Thu, 11 Sep 2014 19:39:48 +0200 blanchet renamed example theory for consistency
Thu, 11 Sep 2014 19:38:22 +0200 blanchet updated ROOT
Thu, 11 Sep 2014 19:26:59 +0200 blanchet renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
Thu, 11 Sep 2014 19:20:23 +0200 blanchet move datatype benchmarks
Mon, 01 Sep 2014 16:17:46 +0200 blanchet took out legacy material from 'HOL/Library/Library.thy'
Mon, 25 Aug 2014 09:40:50 +0200 Andreas Lochbihler add testing framework for generated code
less more (0) -100 -60 tip