src/HOL/ROOT
2014-08-19 Andreas Lochbihler rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
2014-08-19 blanchet avoid old 'smt' method in examples
2014-07-24 wenzelm proper scope of comments;
2014-07-21 traytel regression test for datatypes defined in IsaFoR
2014-07-20 wenzelm proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
2014-07-11 Andreas Lochbihler reactivate session Quickcheck_Examples
2014-07-11 Andreas Lochbihler adapt and reactivate Quickcheck_Types and add two test cases
2014-07-04 wenzelm revived unchecked theory (see cebaf814ca6e);
2014-06-29 blanchet use SMT2
2014-05-22 wenzelm include Nominal2 keywords -- Proof General legacy;
2014-05-19 hoelzl fixed document generation for HOL-Probability
2014-05-11 webertj Replaced refute with nitpick.
2014-05-09 haftmann removed junk from library theory
2014-05-01 boehmes use SMT2 for Boogie examples
2014-05-01 boehmes added internal proof-producing SAT solver
2014-04-30 wenzelm some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
2014-04-29 wenzelm systematic replacement of 'files' by 'document_files';
2014-04-24 haftmann now covered by AFP 3ddac3e572cf
2014-04-23 kuncar all BNF tests can be part of a normal session because they are much faster now
2014-04-08 blanchet added 'datatype_compat' examples/tests
2014-03-19 paulson New complex analysis material
2014-03-13 blanchet use 'smt2' in SMT examples as much as currently possible
2014-03-07 wenzelm tuned whitespace;
2014-02-24 paulson Gauss.thy ported from Old_Number_Theory (unfinished)
2014-02-21 wenzelm more standard theory name;
2014-02-19 haftmann offical tool
2014-02-19 sultana reconstruction framework for LEO-II's TPTP proofs;
2014-02-13 wenzelm reactivate some examples that still appear to work;
2014-02-13 wenzelm do not redefine outer syntax commands;
2014-02-12 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
2014-02-09 wenzelm minimal document;
2014-02-04 paulson Restoration of Pocklington.thy. Tidying.
2014-02-01 wenzelm proper config options;
2014-01-29 paulson Replacing the theory Library/Binomial by Number_Theory/Binomial
2014-01-23 wenzelm no document for Cartouche_Examples: avoid problems typesetting "\001";
2014-01-20 blanchet dissolved BNF session
2014-01-20 blanchet minimized Nitpick's dependencies
2014-01-20 blanchet moved BNF examples
2014-01-20 blanchet killed obsolete session
2014-01-20 blanchet moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
2014-01-18 wenzelm support for nested text cartouches;
2014-01-16 blanchet moved 'Zorn' into 'Main', since it's a BNF dependency
2014-01-10 traytel new codatatype example: stream processors
2013-11-18 blanchet compile
2013-11-18 blanchet split 'Cardinal_Arithmetic' 3-way
2013-11-18 blanchet started three-way split of 'HOL-Cardinals'
2013-11-16 wenzelm merged
2013-11-16 wenzelm proper thy_load command 'boogie_file' -- avoid direct access to file-system;
2013-11-14 haftmann explicit inclusion of data refinement theory into HOL-Library session
2013-10-23 blanchet added 'primcorec' examples
2013-09-26 wenzelm added Isabelle/ML example;
2013-09-23 blanchet register codatatypes with Nitpick
2013-09-17 kuncar include Int_Pow into Quotient_Examples; add end of the theory
2013-09-06 noschinl added examples for Simps_Case_Conv
2013-08-30 blanchet added example
2013-08-23 wenzelm clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
2013-08-21 blanchet renamed theory files to be closer to (new) command names
2013-07-24 nipkow merged Def_Init_Sound_X into Def_Init_X
2013-07-23 boehmes removed obsolete HOL-Boogie session;
2013-07-02 wenzelm clarified Proofterm.proofs vs. Goal.skip_proofs;
less more (0) -100 -60 tip