| Sun, 22 Jul 2012 09:56:34 +0200 |
library theories for debugging and parallel computing using code generation towards Isabelle/ML
|
file | diff | annotate |
| Mon, 28 May 2012 02:18:46 +0200 |
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
|
file | diff | annotate |
| Wed, 30 May 2012 16:05:06 +0200 |
remove pretty syntax for FinFuns at the end and provide separate syntax theory
|
file | diff | annotate |
| Tue, 29 May 2012 15:31:58 +0200 |
move FinFuns from AFP to repository
|
file | diff | annotate |
| Sat, 21 Apr 2012 13:49:31 +0200 |
new example theory for transfer package
|
file | diff | annotate |
| Sat, 14 Apr 2012 19:29:31 +0200 |
removed HOL/ex/Set_Algebras -- outdated clone, obsolete as example
|
file | diff | annotate |
| Fri, 30 Mar 2012 14:27:29 +0200 |
remove content-free theory ex/Arithmetic_Series_Complex.thy
|
file | diff | annotate |
| Sun, 25 Mar 2012 20:15:39 +0200 |
merged fork with new numeral representation (see NEWS)
|
file | diff | annotate |
| Wed, 22 Feb 2012 08:01:41 +0100 |
moving Quickcheck's example to its own session
|
file | diff | annotate |
| Tue, 21 Feb 2012 09:17:53 +0100 |
renamed ex/Numeral.thy to ex/Numeral_Representation.thy
|
file | diff | annotate |
| Thu, 02 Feb 2012 10:12:11 +0100 |
adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
|
file | diff | annotate |
| Fri, 21 Oct 2011 08:42:11 +0200 |
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
|
file | diff | annotate |
| Wed, 21 Sep 2011 17:43:13 -0700 |
HOL/ex/ROOT.ML: only list BinEx once
|
file | diff | annotate |
| Sun, 18 Sep 2011 13:39:33 +0200 |
finite sequences as useful as introductory example;
|
file | diff | annotate |
| Thu, 18 Aug 2011 13:10:24 +0200 |
avoid case-sensitive name for example theory
|
file | diff | annotate |
| Thu, 11 Aug 2011 09:41:21 +0200 |
removed obsolete recdef-related examples
|
file | diff | annotate |
| Mon, 25 Jul 2011 10:43:14 +0200 |
removing SML_Quickcheck
|
file | diff | annotate |
| Wed, 13 Jul 2011 22:16:19 +0200 |
cleanly separate TPTP related files from other examples
|
file | diff | annotate |
| Tue, 07 Jun 2011 11:24:16 +0200 |
merged; manually merged IsaMakefile
|
file | diff | annotate |
| Tue, 07 Jun 2011 11:10:57 +0200 |
renaming the formalisation of the birthday problem to a proper English name
|
file | diff | annotate |
| Tue, 07 Jun 2011 07:04:53 +0200 |
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
|
file | diff | annotate |
| Mon, 02 May 2011 13:29:47 +0200 |
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
|
file | diff | annotate |
| Mon, 02 May 2011 12:09:33 +0200 |
renamed theory to make its purpose clearer
|
file | diff | annotate |
| Wed, 30 Mar 2011 10:31:02 +0200 |
adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape
|
file | diff | annotate |
| Wed, 23 Mar 2011 20:57:37 +0100 |
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
|
file | diff | annotate |
| Wed, 23 Mar 2011 10:06:27 +0100 |
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
|
file | diff | annotate |
| Sun, 13 Mar 2011 19:16:19 +0100 |
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
|
file | diff | annotate |
| Fri, 11 Mar 2011 15:21:13 +0100 |
adapting Quickcheck_Narrowing and example file to new names
|
file | diff | annotate |
| Fri, 11 Mar 2011 10:37:45 +0100 |
only testing theory LSC_Examples when GHC is installed on the machine
|
file | diff | annotate |
| Fri, 11 Mar 2011 10:37:41 +0100 |
adding lazysmallcheck example theory to HOL-ex session
|
file | diff | annotate |
| Sat, 15 Jan 2011 20:05:29 +0100 |
experimental variant of interpretation with simultaneous definitions, plus example
|
file | diff | annotate |
| Fri, 07 Jan 2011 18:10:43 +0100 |
adding example theory for list comprehension to set comprehension simproc
|
file | diff | annotate |
| Wed, 29 Dec 2010 17:34:41 +0100 |
explicit file specifications -- avoid secondary load path;
|
file | diff | annotate |
| Fri, 03 Dec 2010 21:30:41 +0100 |
eliminated fragile HTML.with_charset -- always use utf-8;
|
file | diff | annotate |
| Mon, 22 Nov 2010 10:41:52 +0100 |
adding birthday paradoxon from some abandoned drawer
|
file | diff | annotate |
| Wed, 03 Nov 2010 12:20:33 +0100 |
moved theory Quicksort from Library/ to ex/
|
file | diff | annotate |
| Fri, 29 Oct 2010 21:34:07 +0200 |
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
|
file | diff | annotate |
| Thu, 28 Oct 2010 22:39:59 +0200 |
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
|
file | diff | annotate |
| Wed, 15 Sep 2010 13:44:10 +0200 |
more explicit theory name
|
file | diff | annotate |
| Mon, 06 Sep 2010 14:18:16 +0200 |
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 |
| Mon, 06 Sep 2010 13:06:27 +0200 |
some results of concurrency code inspection;
|
file | diff | annotate |
| Wed, 21 Jul 2010 18:11:51 +0200 |
added new theories to IsaMakefile and ROOT.ML
|
file | diff | annotate |
| Fri, 09 Jul 2010 17:15:03 +0200 |
moved example to its own file in HOL/ex
|
file | diff | annotate |
| Fri, 02 Jul 2010 14:23:18 +0200 |
introduced distinct session HOL-Codegenerator_Test
|
file | diff | annotate |
| Wed, 02 Jun 2010 13:18:21 +0200 |
Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;
|
file | diff | annotate |
| Mon, 17 May 2010 10:58:31 +0200 |
dropped old Library/Word.thy and toy example ex/Adder.thy
|
file | diff | annotate |
| Mon, 10 May 2010 11:30:05 -0700 |
put construction of reals using Dedekind cuts in HOL/ex
|
file | diff | annotate |
| Wed, 24 Mar 2010 17:40:43 +0100 |
moved further predicate compile files to HOL-Library
|
file | diff | annotate |
| Wed, 24 Mar 2010 17:40:43 +0100 |
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
|
file | diff | annotate |
| Tue, 23 Feb 2010 17:33:03 +0100 |
Moved old Integration to examples.
|
file | diff | annotate |
| Wed, 17 Feb 2010 10:43:20 +0100 |
added simple theory about discrete summation
|
file | diff | annotate |
| Wed, 17 Feb 2010 09:48:53 +0100 |
a draft for an example how to turn specifications involving choice executable
|
file | diff | annotate |
| Thu, 12 Nov 2009 20:39:02 +0100 |
adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
|
file | diff | annotate |
| Tue, 10 Nov 2009 13:17:50 +0100 |
try SAT_Examples last, to minimize impact of global side-effects;
|
file | diff | annotate |
| Fri, 06 Nov 2009 14:42:42 +0100 |
renamed method induct_scheme to induction_schema
|
file | diff | annotate |
| Wed, 04 Nov 2009 16:54:22 +0100 |
New
|
file | diff | annotate |
| Fri, 30 Oct 2009 13:59:49 +0100 |
moved Commutative_Ring into session Decision_Procs
|
file | diff | annotate |
| Sun, 20 Sep 2009 18:15:07 +0200 |
Hilbert_Classical: more precise control of parallel_proofs;
|
file | diff | annotate |
| Fri, 11 Sep 2009 09:04:51 +0200 |
corrected upper/lowercase
|
file | diff | annotate |
| Thu, 10 Sep 2009 15:23:08 +0200 |
split of test examples from NatTransfer
|
file | diff | annotate |