| Wed, 22 Feb 2012 08:01:41 +0100 |
bulwahn |
moving Quickcheck's example to its own session
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 09:17:53 +0100 |
huffman |
renamed ex/Numeral.thy to ex/Numeral_Representation.thy
|
file |
diff |
annotate
|
| Thu, 02 Feb 2012 10:12:11 +0100 |
bulwahn |
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 |
huffman |
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 17:43:13 -0700 |
huffman |
HOL/ex/ROOT.ML: only list BinEx once
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 13:39:33 +0200 |
wenzelm |
finite sequences as useful as introductory example;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:10:24 +0200 |
haftmann |
avoid case-sensitive name for example theory
|
file |
diff |
annotate
|
| Thu, 11 Aug 2011 09:41:21 +0200 |
krauss |
removed obsolete recdef-related examples
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 10:43:14 +0200 |
bulwahn |
removing SML_Quickcheck
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
cleanly separate TPTP related files from other examples
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 11:24:16 +0200 |
bulwahn |
merged; manually merged IsaMakefile
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 11:10:57 +0200 |
bulwahn |
renaming the formalisation of the birthday problem to a proper English name
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 07:04:53 +0200 |
blanchet |
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
|
file |
diff |
annotate
|
| Mon, 02 May 2011 13:29:47 +0200 |
blanchet |
fix ROOT.ML and handle "readable_names" reference slightly more cleanly
|
file |
diff |
annotate
|
| Mon, 02 May 2011 12:09:33 +0200 |
blanchet |
renamed theory to make its purpose clearer
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 10:31:02 +0200 |
bulwahn |
adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape
|
file |
diff |
annotate
|
| Wed, 23 Mar 2011 20:57:37 +0100 |
wenzelm |
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
|
file |
diff |
annotate
|
| Wed, 23 Mar 2011 10:06:27 +0100 |
blanchet |
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 19:16:19 +0100 |
wenzelm |
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 |
bulwahn |
adapting Quickcheck_Narrowing and example file to new names
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 10:37:45 +0100 |
bulwahn |
only testing theory LSC_Examples when GHC is installed on the machine
|
file |
diff |
annotate
|
| Fri, 11 Mar 2011 10:37:41 +0100 |
bulwahn |
adding lazysmallcheck example theory to HOL-ex session
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 20:05:29 +0100 |
haftmann |
experimental variant of interpretation with simultaneous definitions, plus example
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 18:10:43 +0100 |
bulwahn |
adding example theory for list comprehension to set comprehension simproc
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 21:30:41 +0100 |
wenzelm |
eliminated fragile HTML.with_charset -- always use utf-8;
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:41:52 +0100 |
bulwahn |
adding birthday paradoxon from some abandoned drawer
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 12:20:33 +0100 |
haftmann |
moved theory Quicksort from Library/ to ex/
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 21:34:07 +0200 |
wenzelm |
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 22:39:59 +0200 |
wenzelm |
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
|
file |
diff |
annotate
|