src/HOL/ROOT
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;
2014-02-19 haftmann 2014-02-19 offical tool
2014-02-19 sultana 2014-02-19 reconstruction framework for LEO-II's TPTP proofs;
2014-02-13 wenzelm 2014-02-13 reactivate some examples that still appear to work;
2014-02-13 wenzelm 2014-02-13 do not redefine outer syntax commands;
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-09 wenzelm 2014-02-09 minimal document;
2014-02-04 paulson 2014-02-04 Restoration of Pocklington.thy. Tidying.
2014-02-01 wenzelm 2014-02-01 proper config options; proper context for printing;
2014-01-29 paulson 2014-01-29 Replacing the theory Library/Binomial by Number_Theory/Binomial
2014-01-23 wenzelm 2014-01-23 no document for Cartouche_Examples: avoid problems typesetting "\001";
2014-01-20 blanchet 2014-01-20 dissolved BNF session
2014-01-20 blanchet 2014-01-20 minimized Nitpick's dependencies
2014-01-20 blanchet 2014-01-20 moved BNF examples
2014-01-20 blanchet 2014-01-20 killed obsolete session
2014-01-20 blanchet 2014-01-20 moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2014-01-16 blanchet 2014-01-16 moved 'Zorn' into 'Main', since it's a BNF dependency
2014-01-10 traytel 2014-01-10 new codatatype example: stream processors
2013-11-18 blanchet 2013-11-18 compile
2013-11-18 blanchet 2013-11-18 split 'Cardinal_Arithmetic' 3-way