src/HOL/ROOT
2015-03-18 noschinl 2015-03-18 added proof method rewrite
2015-03-10 paulson 2015-03-10 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2015-02-10 wenzelm 2015-02-10 check unused theory;
2015-01-25 wenzelm 2015-01-25 discontinued obsolete option "document_graph";
2014-12-28 kleing 2014-12-28 3 old example lemmas by Amine listed in the top 100 theorems
2014-12-20 wenzelm 2014-12-20 afford full test, with slightly improved scheduling order;
2014-12-17 hoelzl 2014-12-17 unfortunately, there is no general function space in the measurable spaces
2014-12-04 wenzelm 2014-12-04 more examples;
2014-11-14 wenzelm 2014-11-14 no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
2014-10-31 wenzelm 2014-10-31 discontinued pointless option: timing is always on (overall theory only);
2014-10-31 wenzelm 2014-10-31 discontinued Proof General;
2014-10-10 nipkow 2014-10-10 New example Bubblesort
2014-10-08 wenzelm 2014-10-08 simplified "sos" method;
2014-10-08 Andreas Lochbihler 2014-10-08 move Code_Test to HOL/Library; add corresponding entries in NEWS and CONTRIBUTORS
2014-10-07 wenzelm 2014-10-07 more bibtex entries; more antiquotations;
2014-09-24 blanchet 2014-09-24 made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow
2014-09-22 wenzelm 2014-09-22 clarified timeout for isatest;
2014-09-22 wenzelm 2014-09-22 examples for local CSDP executable;
2014-09-22 wenzelm 2014-09-22 clarified SOS tool setup vs. examples;
2014-09-22 wenzelm 2014-09-22 clarified ISABELLE_POLYML; added some isatests -- ISABELLE_SCALA still inactive due to problems with case-insensible file-system;
2014-09-21 wenzelm 2014-09-21 renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
2014-09-19 traytel 2014-09-19 regression tests for n2m
2014-09-18 blanchet 2014-09-18 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again
2014-09-18 blanchet 2014-09-18 increased 'HOL-Proofs' timeout
2014-09-18 blanchet 2014-09-18 renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
2014-09-16 blanchet 2014-09-16 took out 'old_datatype' examples -- those just cause timeouts in Isatests
2014-09-12 blanchet 2014-09-12 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
2014-09-12 blanchet 2014-09-12 run larger nominal examples only 'ISABELLE_FULL_TEST'
2014-09-11 blanchet 2014-09-11 renamed example theory for consistency
2014-09-11 blanchet 2014-09-11 updated ROOT
2014-09-11 blanchet 2014-09-11 renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
2014-09-11 blanchet 2014-09-11 move datatype benchmarks
2014-09-01 blanchet 2014-09-01 took out legacy material from 'HOL/Library/Library.thy'
2014-08-25 Andreas Lochbihler 2014-08-25 add testing framework for generated code
2014-08-22 haftmann 2014-08-22 generic euclidean algorithm (due to Manuel Eberl)
2014-08-19 Andreas Lochbihler 2014-08-19 rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
2014-08-19 blanchet 2014-08-19 avoid old 'smt' method in examples
2014-07-24 wenzelm 2014-07-24 proper scope of comments;
2014-07-21 traytel 2014-07-21 regression test for datatypes defined in IsaFoR
2014-07-20 wenzelm 2014-07-20 proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
2014-07-11 Andreas Lochbihler 2014-07-11 reactivate session Quickcheck_Examples
2014-07-11 Andreas Lochbihler 2014-07-11 adapt and reactivate Quickcheck_Types and add two test cases
2014-07-04 wenzelm 2014-07-04 revived unchecked theory (see cebaf814ca6e);
2014-06-29 blanchet 2014-06-29 use SMT2
2014-05-22 wenzelm 2014-05-22 include Nominal2 keywords -- Proof General legacy;
2014-05-19 hoelzl 2014-05-19 fixed document generation for HOL-Probability
2014-05-12 webertj 2014-05-12 Replaced refute with nitpick.
2014-05-09 haftmann 2014-05-09 removed junk from library theory
2014-05-01 boehmes 2014-05-01 use SMT2 for Boogie examples
2014-05-01 boehmes 2014-05-01 added internal proof-producing SAT solver
2014-04-30 wenzelm 2014-04-30 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
2014-04-29 wenzelm 2014-04-29 systematic replacement of 'files' by 'document_files';
2014-04-24 haftmann 2014-04-24 now covered by AFP 3ddac3e572cf
2014-04-23 kuncar 2014-04-23 all BNF tests can be part of a normal session because they are much faster now
2014-04-08 blanchet 2014-04-08 added 'datatype_compat' examples/tests
2014-03-19 paulson 2014-03-19 New complex analysis material
2014-03-13 blanchet 2014-03-13 use 'smt2' in SMT examples as much as currently possible
2014-03-07 wenzelm 2014-03-07 tuned whitespace;
2014-02-24 paulson 2014-02-24 Gauss.thy ported from Old_Number_Theory (unfinished)
2014-02-21 wenzelm 2014-02-21 more standard theory name;