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