2011-10-21 huffman 2011-10-21 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
2011-09-21 huffman 2011-09-21 HOL/ex/ROOT.ML: only list BinEx once
2011-09-18 wenzelm 2011-09-18 finite sequences as useful as introductory example;
2011-08-18 haftmann 2011-08-18 avoid case-sensitive name for example theory
2011-08-11 krauss 2011-08-11 removed obsolete recdef-related examples
2011-07-25 bulwahn 2011-07-25 removing SML_Quickcheck
2011-07-13 blanchet 2011-07-13 cleanly separate TPTP related files from other examples
2011-06-07 bulwahn 2011-06-07 merged; manually merged IsaMakefile
2011-06-07 bulwahn 2011-06-07 renaming the formalisation of the birthday problem to a proper English name
2011-06-07 blanchet 2011-06-07 renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
2011-05-02 blanchet 2011-05-02 fix ROOT.ML and handle "readable_names" reference slightly more cleanly
2011-05-02 blanchet 2011-05-02 renamed theory to make its purpose clearer
2011-03-30 bulwahn 2011-03-30 adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape
2011-03-23 wenzelm 2011-03-23 isolate change of Proofterm.proofs in TPTP.thy from rest of session; qualified Proofterm.proofs to facilitate grepping;
2011-03-23 blanchet 2011-03-23 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" default to "e" rather than "vampire" since E is part of the Isabelle bundle
2011-03-13 wenzelm 2011-03-13 cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection; determine swipl_version at runtime;
2011-03-11 bulwahn 2011-03-11 adapting Quickcheck_Narrowing and example file to new names
2011-03-11 bulwahn 2011-03-11 only testing theory LSC_Examples when GHC is installed on the machine
2011-03-11 bulwahn 2011-03-11 adding lazysmallcheck example theory to HOL-ex session
2011-01-15 haftmann 2011-01-15 experimental variant of interpretation with simultaneous definitions, plus example
2011-01-07 bulwahn 2011-01-07 adding example theory for list comprehension to set comprehension simproc
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-03 wenzelm 2010-12-03 eliminated fragile HTML.with_charset -- always use utf-8;
2010-11-22 bulwahn 2010-11-22 adding birthday paradoxon from some abandoned drawer
2010-11-03 haftmann 2010-11-03 moved theory Quicksort from Library/ to ex/
2010-10-29 wenzelm 2010-10-29 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
2010-10-28 wenzelm 2010-10-28 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; tuned;
2010-09-15 haftmann 2010-09-15 more explicit theory name
2010-09-06 wenzelm 2010-09-06 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 wenzelm 2010-09-06 some results of concurrency code inspection;
2010-07-21 bulwahn 2010-07-21 added new theories to IsaMakefile and ROOT.ML
2010-07-09 krauss 2010-07-09 moved example to its own file in HOL/ex
2010-07-02 haftmann 2010-07-02 introduced distinct session HOL-Codegenerator_Test
2010-06-02 wenzelm 2010-06-02 Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;
2010-05-17 haftmann 2010-05-17 dropped old Library/Word.thy and toy example ex/Adder.thy
2010-05-10 huffman 2010-05-10 put construction of reals using Dedekind cuts in HOL/ex
2010-03-24 bulwahn 2010-03-24 moved further predicate compile files to HOL-Library
2010-03-24 bulwahn 2010-03-24 moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
2010-02-23 hoelzl 2010-02-23 Moved old Integration to examples.
2010-02-17 haftmann 2010-02-17 added simple theory about discrete summation
2010-02-17 haftmann 2010-02-17 a draft for an example how to turn specifications involving choice executable
2009-11-12 bulwahn 2009-11-12 adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
2009-11-10 wenzelm 2009-11-10 try SAT_Examples last, to minimize impact of global side-effects;
2009-11-06 krauss 2009-11-06 renamed method induct_scheme to induction_schema
2009-11-04 nipkow 2009-11-04 New
2009-10-30 haftmann 2009-10-30 moved Commutative_Ring into session Decision_Procs
2009-09-20 wenzelm 2009-09-20 Hilbert_Classical: more precise control of parallel_proofs;
2009-09-11 haftmann 2009-09-11 corrected upper/lowercase
2009-09-10 haftmann 2009-09-10 split of test examples from NatTransfer
2009-09-01 haftmann 2009-09-01 some reorganization of number theory
2009-08-28 wenzelm 2009-08-28 SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably; misc tuning and cleanup;
2009-07-28 wenzelm 2009-07-28 Future.shutdown before loading sequentially -- workaround scheduler deadlock;
2009-07-28 wenzelm 2009-07-28 Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
2009-07-28 wenzelm 2009-07-28 non-critical use_thy;
2009-07-24 wenzelm 2009-07-24 removed Formal_Power_Series_Examples (cf. adea7a729c7a);
2009-07-22 wenzelm 2009-07-22 shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;
2009-06-11 haftmann 2009-06-11 merged
2009-06-09 haftmann 2009-06-09 first running version of qc generators for datatypes
2009-06-11 wenzelm 2009-06-11 merged, reverting workarounds on both sides;
2009-06-11 wenzelm 2009-06-11 theory Predicate_Compile_ex: enable quick_and_dirty for now, to make it work with internal cheat_tac invocations;