2012-03-25 ago merged fork with new numeral representation (see NEWS)
2012-02-22 ago moving Quickcheck's example to its own session
2012-02-21 ago renamed ex/Numeral.thy to ex/Numeral_Representation.thy
2012-02-02 ago adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
2011-10-21 ago add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
2011-09-21 ago HOL/ex/ROOT.ML: only list BinEx once
2011-09-18 ago finite sequences as useful as introductory example;
2011-08-18 ago avoid case-sensitive name for example theory
2011-08-11 ago removed obsolete recdef-related examples
2011-07-25 ago removing SML_Quickcheck
2011-07-13 ago cleanly separate TPTP related files from other examples
2011-06-07 ago merged; manually merged IsaMakefile
2011-06-07 ago renaming the formalisation of the birthday problem to a proper English name
2011-06-07 ago renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
2011-05-02 ago fix ROOT.ML and handle "readable_names" reference slightly more cleanly
2011-05-02 ago renamed theory to make its purpose clearer
2011-03-30 ago adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape
2011-03-23 ago isolate change of Proofterm.proofs in TPTP.thy from rest of session;
2011-03-23 ago move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
2011-03-13 ago cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
2011-03-11 ago adapting Quickcheck_Narrowing and example file to new names
2011-03-11 ago only testing theory LSC_Examples when GHC is installed on the machine
2011-03-11 ago adding lazysmallcheck example theory to HOL-ex session
2011-01-15 ago experimental variant of interpretation with simultaneous definitions, plus example
2011-01-07 ago adding example theory for list comprehension to set comprehension simproc
2010-12-29 ago explicit file specifications -- avoid secondary load path;
2010-12-03 ago eliminated fragile HTML.with_charset -- always use utf-8;
2010-11-22 ago adding birthday paradoxon from some abandoned drawer
2010-11-03 ago moved theory Quicksort from Library/ to ex/
2010-10-29 ago Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
2010-10-28 ago moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
2010-09-15 ago more explicit theory name
2010-09-06 ago more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
2010-09-06 ago some results of concurrency code inspection;
2010-07-21 ago added new theories to IsaMakefile and ROOT.ML
2010-07-09 ago moved example to its own file in HOL/ex
2010-07-02 ago introduced distinct session HOL-Codegenerator_Test
2010-06-02 ago Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;
2010-05-17 ago dropped old Library/Word.thy and toy example ex/Adder.thy
2010-05-10 ago put construction of reals using Dedekind cuts in HOL/ex
2010-03-24 ago moved further predicate compile files to HOL-Library
2010-03-24 ago moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
2010-02-23 ago Moved old Integration to examples.
2010-02-17 ago added simple theory about discrete summation
2010-02-17 ago a draft for an example how to turn specifications involving choice executable
2009-11-12 ago adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
2009-11-10 ago try SAT_Examples last, to minimize impact of global side-effects;
2009-11-06 ago renamed method induct_scheme to induction_schema
2009-11-04 ago New
2009-10-30 ago moved Commutative_Ring into session Decision_Procs
2009-09-20 ago Hilbert_Classical: more precise control of parallel_proofs;
2009-09-11 ago corrected upper/lowercase
2009-09-10 ago split of test examples from NatTransfer
2009-09-01 ago some reorganization of number theory
2009-08-28 ago SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
2009-07-28 ago Future.shutdown before loading sequentially -- workaround scheduler deadlock;
2009-07-28 ago Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
2009-07-28 ago non-critical use_thy;
2009-07-24 ago removed Formal_Power_Series_Examples (cf. adea7a729c7a);
2009-07-22 ago shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;