| 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
|
| Tue, 03 Aug 1999 13:15:54 +0200 |
paulson |
new examples file for SVC
|
file |
diff |
annotate
|
| Mon, 26 Jul 1999 16:30:50 +0200 |
paulson |
HOL/ex/Tarski: new example by Florian Kammueller
|
file |
diff |
annotate
|
| Thu, 11 Mar 1999 13:20:35 +0100 |
wenzelm |
removed foo_build_completed -- now handled by session management (via usedir);
|
file |
diff |
annotate
|
| Mon, 16 Nov 1998 10:37:54 +0100 |
paulson |
removed the reference to mesontest2.ML, itself now deleted
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 20:28:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 24 Aug 1998 18:17:25 +0200 |
wenzelm |
added Antiquote example;
|
file |
diff |
annotate
|
| Tue, 04 Aug 1998 18:40:18 +0200 |
wenzelm |
added LocaleGroup, PiSets examples;
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 17:55:57 +0200 |
wenzelm |
added ex/MonoidGroups (record example);
|
file |
diff |
annotate
|
| Fri, 03 Jul 1998 17:35:39 +0200 |
wenzelm |
stepping stones: Recdef, Main;
|
file |
diff |
annotate
|
| Thu, 25 Jun 1998 13:57:34 +0200 |
paulson |
Installation of target HOL-Real
|
file |
diff |
annotate
|
| Mon, 20 Apr 1998 10:37:00 +0200 |
paulson |
proving fib(gcd(m,n)) = gcd(fib m, fib n)
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 10:28:33 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 13:26:09 +0200 |
paulson |
Now loads theory Recdef
|
file |
diff |
annotate
|
| Mon, 26 May 1997 12:34:05 +0200 |
paulson |
Primrec: New example ported from ZF
|
file |
diff |
annotate
|
| Thu, 22 May 1997 15:08:14 +0200 |
paulson |
New example: ex/Fib
|
file |
diff |
annotate
|
| Tue, 20 May 1997 11:44:25 +0200 |
paulson |
Removal of ex/LexProd
|
file |
diff |
annotate
|
| Wed, 07 May 1997 13:51:22 +0200 |
paulson |
Moved induction examples to directory Induct
|
file |
diff |
annotate
|
| Fri, 18 Apr 1997 11:53:55 +0200 |
paulson |
Now loads theory LList indirectly: via LFilter
|
file |
diff |
annotate
|
| Fri, 29 Nov 1996 15:08:06 +0100 |
nipkow |
Moved the Rings stuff from ex to Integ and showed that int::cring.
|
file |
diff |
annotate
|
| Tue, 26 Nov 1996 14:26:38 +0100 |
nipkow |
Added Lagrang. Modified comment.
|
file |
diff |
annotate
|