src/HOL/ex/ROOT.ML
Mon, 12 Jul 2004 12:11:46 +0200 nipkow *** empty log message ***
Fri, 16 Apr 2004 20:33:16 +0200 nipkow Moved ring stuff from ex into Ring_and_Field.
Fri, 16 Apr 2004 18:09:24 +0200 berghofe Added theory with examples for quickcheck command.
Thu, 15 Apr 2004 14:17:45 +0200 nipkow Added ex/Exceptions.thy
Mon, 29 Mar 2004 15:35:04 +0200 skalberg Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
Thu, 25 Mar 2004 05:37:32 +0100 kleing moved MiniML and AVL to archive of formal proofs
Thu, 11 Mar 2004 11:24:54 +0100 webertj Refute_Examples added/fixed
Wed, 10 Mar 2004 22:39:12 +0100 webertj added Refute_Examples.thy
Wed, 22 Oct 2003 10:52:36 +0200 paulson InductiveInvariant_examples illustrates advanced recursive function definitions
Wed, 08 Oct 2003 15:57:41 +0200 paulson Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
Tue, 25 Mar 2003 09:50:53 +0100 berghofe Added examples for Presburger arithmetic.
Mon, 03 Jun 2002 09:36:30 +0200 nipkow Added ex/MergeSort
Tue, 05 Feb 2002 23:18:08 +0100 wenzelm moved SVC stuff to ex;
Mon, 10 Dec 2001 15:36:05 +0100 berghofe Added example file for intuitionistic logic (taken from FOL).
Tue, 04 Dec 2001 17:59:36 +0100 wenzelm added Higher_Order_Logic.thy;
Fri, 23 Nov 2001 19:19:35 +0100 wenzelm time_use_thy "Locales";
Thu, 22 Nov 2001 23:46:33 +0100 wenzelm theory Locales temporarily disabled;
Fri, 09 Nov 2001 00:11:52 +0100 wenzelm back to normal;
Thu, 08 Nov 2001 23:50:08 +0100 wenzelm tuned;
Tue, 06 Nov 2001 23:51:16 +0100 wenzelm use_thy "Locales";
Thu, 27 Sep 2001 15:42:08 +0200 wenzelm tuned;
Mon, 23 Jul 2001 17:45:35 +0200 paulson PiSets moved to GroupTheory, while LocaleGroup deleted
Fri, 10 Nov 2000 19:08:30 +0100 wenzelm proper theory context for mesontest2;
Thu, 21 Sep 2000 15:58:13 +0200 wenzelm renamed HOL/ex/Points to HOL/ex/Records;
Wed, 13 Sep 2000 18:45:10 +0200 paulson moved Primes, Fib, Factorization to HOL/NumberTheory
Tue, 05 Sep 2000 10:15:23 +0200 paulson meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
Sun, 16 Jul 2000 20:49:33 +0200 wenzelm added Tuple.thy;
Thu, 13 Jul 2000 11:41:40 +0200 wenzelm tuned;
Wed, 21 Jun 2000 15:58:23 +0200 wenzelm fixed deps;
Tue, 30 May 2000 16:08:38 +0200 wenzelm cleaned up;
Wed, 24 May 2000 12:21:26 +0200 paulson restored NatSum.thy
Tue, 23 May 2000 12:36:36 +0200 paulson theory file NatSum.thy no longer needed
Fri, 05 May 2000 12:51:33 +0200 nipkow Added AVL
Fri, 24 Mar 2000 17:28:03 +0100 wenzelm added HOL/ex/Multiquote.thy;
Thu, 23 Mar 2000 10:22:08 +0100 paulson restored the MESON examples file HOL/ex/mesontest2.ML
Wed, 08 Mar 2000 16:14:12 +0100 paulson new theory ex/Factorization
Fri, 20 Aug 1999 15:41:53 +0200 wenzelm if_svc_enabled;
Fri, 06 Aug 1999 17:28:45 +0200 paulson svc_enabled is now declared as a function
Fri, 06 Aug 1999 11:05:20 +0200 paulson new theory ex/svc_test.thy
Tue, 03 Aug 1999 13:15:54 +0200 paulson new examples file for SVC
Mon, 26 Jul 1999 16:30:50 +0200 paulson HOL/ex/Tarski: new example by Florian Kammueller
Thu, 11 Mar 1999 13:20:35 +0100 wenzelm removed foo_build_completed -- now handled by session management (via usedir);
Mon, 16 Nov 1998 10:37:54 +0100 paulson removed the reference to mesontest2.ML, itself now deleted
Fri, 23 Oct 1998 20:28:33 +0200 wenzelm tuned;
Mon, 24 Aug 1998 18:17:25 +0200 wenzelm added Antiquote example;
Tue, 04 Aug 1998 18:40:18 +0200 wenzelm added LocaleGroup, PiSets examples;
Fri, 24 Jul 1998 17:55:57 +0200 wenzelm added ex/MonoidGroups (record example);
Fri, 03 Jul 1998 17:35:39 +0200 wenzelm stepping stones: Recdef, Main;
Thu, 25 Jun 1998 13:57:34 +0200 paulson Installation of target HOL-Real
Mon, 20 Apr 1998 10:37:00 +0200 paulson proving fib(gcd(m,n)) = gcd(fib m, fib n)
Fri, 19 Dec 1997 10:28:33 +0100 wenzelm tuned;
Thu, 05 Jun 1997 13:26:09 +0200 paulson Now loads theory Recdef
Mon, 26 May 1997 12:34:05 +0200 paulson Primrec: New example ported from ZF
Thu, 22 May 1997 15:08:14 +0200 paulson New example: ex/Fib
Tue, 20 May 1997 11:44:25 +0200 paulson Removal of ex/LexProd
Wed, 07 May 1997 13:51:22 +0200 paulson Moved induction examples to directory Induct
Fri, 18 Apr 1997 11:53:55 +0200 paulson Now loads theory LList indirectly: via LFilter
Fri, 29 Nov 1996 15:08:06 +0100 nipkow Moved the Rings stuff from ex to Integ and showed that int::cring.
Tue, 26 Nov 1996 14:26:38 +0100 nipkow Added Lagrang. Modified comment.
Fri, 14 Jun 1996 12:25:19 +0200 paulson Added new Primes theory
less more (0) -60 tip