Tue, 06 Jan 2009 22:08:42 +0100 |
wenzelm |
more parallel loading;
|
file |
diff |
annotate
|
Tue, 06 Jan 2009 21:55:51 +0100 |
wenzelm |
more parallel loading;
|
file |
diff |
annotate
|
Sat, 27 Dec 2008 17:35:00 +0100 |
krauss |
renamed LexOrds.thy to Termination.thy; examples for sizechange method
|
file |
diff |
annotate
|
Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
Thu, 20 Nov 2008 19:43:34 +0100 |
wenzelm |
reactivated some dead theories (based on hints by Mark Hillebrand);
|
file |
diff |
annotate
|
Thu, 16 Oct 2008 23:21:23 +0200 |
wenzelm |
removed Locales;
|
file |
diff |
annotate
|
Thu, 25 Sep 2008 11:14:01 +0200 |
haftmann |
(temporary workaround)
|
file |
diff |
annotate
|
Thu, 25 Sep 2008 10:17:23 +0200 |
haftmann |
(temporal deactivation)
|
file |
diff |
annotate
|
Mon, 22 Sep 2008 22:59:35 +0200 |
berghofe |
Added examples for coherent logic prover.
|
file |
diff |
annotate
|
Wed, 17 Sep 2008 21:27:14 +0200 |
wenzelm |
moved global ML bindings to global place;
|
file |
diff |
annotate
|
Tue, 16 Sep 2008 16:13:06 +0200 |
haftmann |
moved term_of syntax to separate theory
|
file |
diff |
annotate
|
Tue, 16 Sep 2008 09:21:24 +0200 |
haftmann |
evaluation using code generator
|
file |
diff |
annotate
|
Wed, 03 Sep 2008 12:11:28 +0200 |
nipkow |
removed ex/Puzzle
|
file |
diff |
annotate
|
Wed, 03 Sep 2008 00:11:27 +0200 |
kleing |
retired Ben Porter's DenumRat in favour of the shorter proof in
|
file |
diff |
annotate
|
Tue, 02 Sep 2008 22:37:20 +0200 |
nipkow |
Replaced Library/NatPair by Nat_Int_Bij.
|
file |
diff |
annotate
|
Wed, 27 Aug 2008 12:01:59 +0200 |
haftmann |
added HOL/ex/Numeral.thy
|
file |
diff |
annotate
|
Tue, 05 Aug 2008 14:40:48 +0200 |
krauss |
fix HOL/ex/LexOrds.thy; add to regression
|
file |
diff |
annotate
|
Fri, 25 Jul 2008 12:03:28 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Thu, 03 Jul 2008 20:15:06 +0200 |
wenzelm |
removed old NSPrimes, cf. NSA/Examples/;
|
file |
diff |
annotate
|
Wed, 02 Jul 2008 07:12:17 +0200 |
haftmann |
code antiquotation roaring ahead
|
file |
diff |
annotate
|
Tue, 01 Jul 2008 07:58:17 +0200 |
haftmann |
HOL += HOL-Complex
|
file |
diff |
annotate
|
Wed, 12 Mar 2008 19:38:14 +0100 |
haftmann |
separated Random.thy from Quickcheck.thy
|
file |
diff |
annotate
|
Wed, 20 Feb 2008 23:24:38 +0100 |
wenzelm |
removed NBE;
|
file |
diff |
annotate
|
Fri, 25 Jan 2008 23:05:27 +0100 |
wenzelm |
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
|
file |
diff |
annotate
|
Fri, 25 Jan 2008 14:53:56 +0100 |
haftmann |
distinguished examples for Efficient_Nat.thy
|
file |
diff |
annotate
|
Thu, 20 Dec 2007 22:21:30 +0100 |
wenzelm |
included meson/metis tests in simultaneous use_thys;
|
file |
diff |
annotate
|
Fri, 07 Dec 2007 10:59:03 +0100 |
krauss |
Adding "ex/Induction_Scheme.thy" to tests
|
file |
diff |
annotate
|
Wed, 05 Dec 2007 14:16:15 +0100 |
haftmann |
dropped Classpackage.thy
|
file |
diff |
annotate
|
Sat, 10 Nov 2007 14:36:33 +0100 |
wenzelm |
qualified Proofterm.proofs;
|
file |
diff |
annotate
|
Fri, 12 Oct 2007 08:21:09 +0200 |
haftmann |
consolidated naming conventions for code generator theories
|
file |
diff |
annotate
|
Thu, 11 Oct 2007 23:03:51 +0200 |
wenzelm |
enabled Refute_Examples again;
|
file |
diff |
annotate
|
Thu, 11 Oct 2007 21:44:28 +0200 |
wenzelm |
disabled Refute_Examples temporarily;
|
file |
diff |
annotate
|
Thu, 27 Sep 2007 17:22:15 +0200 |
wenzelm |
some more simultaneous use_thys;
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 05:42:46 +0200 |
nipkow |
Added function package to PreList
|
file |
diff |
annotate
|
Thu, 06 Sep 2007 11:32:28 +0200 |
berghofe |
Integrated Executable_Rat and Executable_Real theories into
|
file |
diff |
annotate
|
Wed, 05 Sep 2007 20:48:25 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 29 Aug 2007 20:18:23 +0200 |
wenzelm |
some simultaneous use_thys;
|
file |
diff |
annotate
|
Thu, 09 Aug 2007 15:52:45 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Thu, 02 Aug 2007 15:44:37 +0200 |
wenzelm |
converted Meson tests to proper theory;
|
file |
diff |
annotate
|
Thu, 19 Jul 2007 21:47:39 +0200 |
haftmann |
uniform naming conventions for CG theories
|
file |
diff |
annotate
|
Mon, 16 Jul 2007 09:29:01 +0200 |
haftmann |
fixed SML/NJ int problem
|
file |
diff |
annotate
|
Tue, 26 Jun 2007 13:01:48 +0200 |
nipkow |
added NBE
|
file |
diff |
annotate
|
Thu, 21 Jun 2007 15:42:07 +0200 |
wenzelm |
replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
|
file |
diff |
annotate
|
Sun, 10 Jun 2007 23:48:27 +0200 |
wenzelm |
disabled theory "Reflected_Presburger" for smlnj (temporarily);
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 22:46:58 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
Fri, 01 Jun 2007 23:21:40 +0200 |
webertj |
some tests for arith added
|
file |
diff |
annotate
|
Fri, 01 Jun 2007 20:34:12 +0200 |
webertj |
MiniSAT mentioned in comment
|
file |
diff |
annotate
|
Thu, 17 May 2007 22:33:41 +0200 |
krauss |
Added unification case study (using new function package)
|
file |
diff |
annotate
|
Fri, 13 Apr 2007 10:00:04 +0200 |
ballarin |
New file for locale regression tests.
|
file |
diff |
annotate
|
Tue, 27 Mar 2007 12:28:42 +0200 |
haftmann |
cleaned up HOL/ex/Code*.thy
|
file |
diff |
annotate
|
Mon, 26 Mar 2007 14:53:05 +0200 |
haftmann |
moved Eval theory to library
|
file |
diff |
annotate
|
Fri, 23 Mar 2007 09:40:47 +0100 |
haftmann |
removed outdated example
|
file |
diff |
annotate
|
Mon, 22 Jan 2007 18:17:04 +0100 |
krauss |
Included ex/Fundefs.thy in HOL-ex session
|
file |
diff |
annotate
|
Sat, 20 Jan 2007 14:27:45 +0100 |
wenzelm |
added HOL/ex/Binary.thy;
|
file |
diff |
annotate
|
Tue, 16 Jan 2007 08:06:55 +0100 |
haftmann |
refined and added example for ExecutableRat
|
file |
diff |
annotate
|
Wed, 27 Dec 2006 19:10:00 +0100 |
haftmann |
added OCaml code generation (without dictionaries)
|
file |
diff |
annotate
|
Wed, 08 Nov 2006 23:11:13 +0100 |
wenzelm |
moved theories Parity, GCD, Binomial to Library;
|
file |
diff |
annotate
|
Fri, 06 Oct 2006 03:49:36 +0200 |
kleing |
examples for hex and bin numerals
|
file |
diff |
annotate
|
Sun, 01 Oct 2006 18:29:31 +0200 |
wenzelm |
reactivated theory PER;
|
file |
diff |
annotate
|
Tue, 19 Sep 2006 15:22:05 +0200 |
haftmann |
code generation 2 adjustments
|
file |
diff |
annotate
|
Wed, 30 Aug 2006 08:34:45 +0200 |
haftmann |
added yet another code generator example
|
file |
diff |
annotate
|
Tue, 29 Aug 2006 14:31:14 +0200 |
haftmann |
added and refined some exmples
|
file |
diff |
annotate
|
Mon, 21 Aug 2006 11:02:39 +0200 |
haftmann |
added some codegen examples/applications
|
file |
diff |
annotate
|
Thu, 03 Aug 2006 15:03:49 +0200 |
wenzelm |
added HOL/ex/Reflection;
|
file |
diff |
annotate
|
Tue, 04 Jul 2006 19:49:47 +0200 |
wenzelm |
added ex/Guess.thy;
|
file |
diff |
annotate
|
Fri, 09 Jun 2006 16:25:05 +0200 |
nipkow |
nbe -> NormalForm
|
file |
diff |
annotate
|
Thu, 13 Apr 2006 12:01:16 +0200 |
wenzelm |
early test of Classpackage, Codegenerator;
|
file |
diff |
annotate
|
Fri, 17 Mar 2006 14:20:24 +0100 |
haftmann |
added example for operational classes and code generator
|
file |
diff |
annotate
|
Sat, 11 Mar 2006 16:53:10 +0100 |
wenzelm |
nbe: no_document;
|
file |
diff |
annotate
|
Mon, 27 Feb 2006 14:34:03 +0100 |
nipkow |
added temp. nbe test
|
file |
diff |
annotate
|
Thu, 16 Feb 2006 21:11:58 +0100 |
wenzelm |
added ex/Abstract_NAT.thy;
|
file |
diff |
annotate
|
Sun, 12 Feb 2006 10:42:19 +0100 |
kleing |
* moved ThreeDivides from Isar_examples to better suited HOL/ex
|
file |
diff |
annotate
|
Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
Wed, 14 Dec 2005 22:05:22 +0100 |
webertj |
ex/Sudoku.thy
|
file |
diff |
annotate
|
Fri, 07 Oct 2005 22:59:21 +0200 |
wenzelm |
removed obsolete ex/Tuple.thy;
|
file |
diff |
annotate
|
Fri, 23 Sep 2005 22:58:50 +0200 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
file |
diff |
annotate
|
Tue, 20 Sep 2005 13:56:34 +0200 |
wenzelm |
Chinese Unicode example;
|
file |
diff |
annotate
|
Sat, 17 Sep 2005 18:11:26 +0200 |
wenzelm |
Hebrew: HTML.with_charset;
|
file |
diff |
annotate
|
Thu, 15 Sep 2005 17:17:01 +0200 |
wenzelm |
added Hebrew.thy;
|
file |
diff |
annotate
|
Wed, 14 Sep 2005 17:25:52 +0200 |
chaieb |
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
|
file |
diff |
annotate
|
Thu, 28 Apr 2005 17:08:08 +0200 |
bauerg |
*** empty log message ***
|
file |
diff |
annotate
|
Mon, 12 Jul 2004 12:11:46 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
Fri, 16 Apr 2004 20:33:16 +0200 |
nipkow |
Moved ring stuff from ex into Ring_and_Field.
|
file |
diff |
annotate
|
Fri, 16 Apr 2004 18:09:24 +0200 |
berghofe |
Added theory with examples for quickcheck command.
|
file |
diff |
annotate
|
Thu, 15 Apr 2004 14:17:45 +0200 |
nipkow |
Added ex/Exceptions.thy
|
file |
diff |
annotate
|
Mon, 29 Mar 2004 15:35:04 +0200 |
skalberg |
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
|
file |
diff |
annotate
|
Thu, 25 Mar 2004 05:37:32 +0100 |
kleing |
moved MiniML and AVL to archive of formal proofs
|
file |
diff |
annotate
|
Thu, 11 Mar 2004 11:24:54 +0100 |
webertj |
Refute_Examples added/fixed
|
file |
diff |
annotate
|
Wed, 10 Mar 2004 22:39:12 +0100 |
webertj |
added Refute_Examples.thy
|
file |
diff |
annotate
|
Wed, 22 Oct 2003 10:52:36 +0200 |
paulson |
InductiveInvariant_examples illustrates advanced recursive function definitions
|
file |
diff |
annotate
|
Wed, 08 Oct 2003 15:57:41 +0200 |
paulson |
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
|
file |
diff |
annotate
|
Tue, 25 Mar 2003 09:50:53 +0100 |
berghofe |
Added examples for Presburger arithmetic.
|
file |
diff |
annotate
|
Mon, 03 Jun 2002 09:36:30 +0200 |
nipkow |
Added ex/MergeSort
|
file |
diff |
annotate
|
Tue, 05 Feb 2002 23:18:08 +0100 |
wenzelm |
moved SVC stuff to ex;
|
file |
diff |
annotate
|
Mon, 10 Dec 2001 15:36:05 +0100 |
berghofe |
Added example file for intuitionistic logic (taken from FOL).
|
file |
diff |
annotate
|
Tue, 04 Dec 2001 17:59:36 +0100 |
wenzelm |
added Higher_Order_Logic.thy;
|
file |
diff |
annotate
|
Fri, 23 Nov 2001 19:19:35 +0100 |
wenzelm |
time_use_thy "Locales";
|
file |
diff |
annotate
|
Thu, 22 Nov 2001 23:46:33 +0100 |
wenzelm |
theory Locales temporarily disabled;
|
file |
diff |
annotate
|
Fri, 09 Nov 2001 00:11:52 +0100 |
wenzelm |
back to normal;
|
file |
diff |
annotate
|
Thu, 08 Nov 2001 23:50:08 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 06 Nov 2001 23:51:16 +0100 |
wenzelm |
use_thy "Locales";
|
file |
diff |
annotate
|
Thu, 27 Sep 2001 15:42:08 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 23 Jul 2001 17:45:35 +0200 |
paulson |
PiSets moved to GroupTheory, while LocaleGroup deleted
|
file |
diff |
annotate
|
Fri, 10 Nov 2000 19:08:30 +0100 |
wenzelm |
proper theory context for mesontest2;
|
file |
diff |
annotate
|
Thu, 21 Sep 2000 15:58:13 +0200 |
wenzelm |
renamed HOL/ex/Points to HOL/ex/Records;
|
file |
diff |
annotate
|
Wed, 13 Sep 2000 18:45:10 +0200 |
paulson |
moved Primes, Fib, Factorization to HOL/NumberTheory
|
file |
diff |
annotate
|
Tue, 05 Sep 2000 10:15:23 +0200 |
paulson |
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
|
file |
diff |
annotate
|
Sun, 16 Jul 2000 20:49:33 +0200 |
wenzelm |
added Tuple.thy;
|
file |
diff |
annotate
|
Thu, 13 Jul 2000 11:41:40 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 21 Jun 2000 15:58:23 +0200 |
wenzelm |
fixed deps;
|
file |
diff |
annotate
|
Tue, 30 May 2000 16:08:38 +0200 |
wenzelm |
cleaned up;
|
file |
diff |
annotate
|
Wed, 24 May 2000 12:21:26 +0200 |
paulson |
restored NatSum.thy
|
file |
diff |
annotate
|
Tue, 23 May 2000 12:36:36 +0200 |
paulson |
theory file NatSum.thy no longer needed
|
file |
diff |
annotate
|
Fri, 05 May 2000 12:51:33 +0200 |
nipkow |
Added AVL
|
file |
diff |
annotate
|
Fri, 24 Mar 2000 17:28:03 +0100 |
wenzelm |
added HOL/ex/Multiquote.thy;
|
file |
diff |
annotate
|
Thu, 23 Mar 2000 10:22:08 +0100 |
paulson |
restored the MESON examples file HOL/ex/mesontest2.ML
|
file |
diff |
annotate
|
Wed, 08 Mar 2000 16:14:12 +0100 |
paulson |
new theory ex/Factorization
|
file |
diff |
annotate
|
Fri, 20 Aug 1999 15:41:53 +0200 |
wenzelm |
if_svc_enabled;
|
file |
diff |
annotate
|
Fri, 06 Aug 1999 17:28:45 +0200 |
paulson |
svc_enabled is now declared as a function
|
file |
diff |
annotate
|
Fri, 06 Aug 1999 11:05:20 +0200 |
paulson |
new theory ex/svc_test.thy
|
file |
diff |
annotate
|