src/HOL/IsaMakefile
Fri, 25 Apr 2003 11:18:41 +0200 paulson Auth: certified email protocol
Fri, 11 Apr 2003 23:11:13 +0200 webertj Map.ML integrated into Map.thy
Wed, 09 Apr 2003 12:51:49 +0200 paulson Removal of Summation theory
Tue, 25 Mar 2003 09:49:45 +0100 berghofe Added decision procedure for Presburger arithmetic.
Sun, 23 Mar 2003 11:57:07 +0100 nipkow *** empty log message ***
Fri, 21 Mar 2003 18:15:56 +0100 paulson quadratic reciprocity files
Tue, 18 Mar 2003 18:07:06 +0100 paulson moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
Tue, 11 Mar 2003 15:19:27 +0100 nipkow *** empty log message ***
Mon, 10 Mar 2003 16:21:06 +0100 paulson New theory ProgressSets. Definition of closure sets
Thu, 06 Mar 2003 15:08:38 +0100 paulson new UNITY examples theory
Tue, 18 Feb 2003 15:09:14 +0100 paulson new theory Transformers: Meier-Sanders non-interference theory
Fri, 31 Jan 2003 20:12:44 +0100 paulson conversion to new-style theories and tidying
Thu, 30 Jan 2003 18:08:09 +0100 paulson conversion of UNITY theories to new-style
Thu, 30 Jan 2003 10:35:56 +0100 paulson converting more UNITY theories to new-style
Wed, 29 Jan 2003 16:34:51 +0100 paulson converted more UNITY theories to new-style
Wed, 29 Jan 2003 11:02:08 +0100 paulson converting UNITY to new-style theories
Mon, 27 Jan 2003 10:39:31 +0100 kleing fixed missing UNITY files
Fri, 24 Jan 2003 14:06:49 +0100 paulson Partial conversion of UNITY to Isar new-style theories
Wed, 08 Jan 2003 13:49:52 +0100 nipkow New files in Hoare/
Wed, 11 Dec 2002 10:12:48 +0100 ballarin HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
Thu, 28 Nov 2002 10:50:42 +0100 ballarin HOL-Algebra partially ported to Isar.
Wed, 13 Nov 2002 15:26:19 +0100 berghofe Added inductive_realizer.
Sat, 09 Nov 2002 00:12:25 +0100 kleing Hoare.ML -> hoare.ML
Wed, 06 Nov 2002 14:02:18 +0100 nipkow Hoare.ML -> hoare.ML
Tue, 05 Nov 2002 15:59:17 +0100 kleing two new Bali files
Mon, 28 Oct 2002 14:29:51 +0100 nipkow conversion ML -> thy
Wed, 23 Oct 2002 16:09:02 +0200 streckem Added compiler
Fri, 27 Sep 2002 10:33:47 +0200 paulson New theory GroupTheory/Module.thy of modules
Thu, 26 Sep 2002 15:21:38 +0200 paulson Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
Thu, 26 Sep 2002 10:51:29 +0200 paulson Converted Fun to Isar style.
Wed, 25 Sep 2002 07:57:36 +0200 nipkow Int.thy -> int.thy
Sat, 31 Aug 2002 14:03:49 +0200 paulson converted Hyperreal/Zorn to Isar format and moved to Library
Fri, 23 Aug 2002 07:41:05 +0200 nipkow Added div+mod cancelling simproc
Wed, 21 Aug 2002 15:53:30 +0200 paulson Frederic Blanqui's new "guard" examples
Thu, 08 Aug 2002 23:46:51 +0200 wenzelm tuned deps;
Wed, 07 Aug 2002 16:48:20 +0200 berghofe Added file Tools/datatype_realizer.ML
Mon, 05 Aug 2002 14:35:33 +0200 berghofe Removed theory NatDef.
Sun, 21 Jul 2002 15:42:30 +0200 berghofe Added theory for setting up program extraction.
Wed, 19 Jun 2002 12:39:41 +0200 kleing LBV instantiantion refactored, streamlined
Mon, 03 Jun 2002 09:36:30 +0200 nipkow Added ex/MergeSort
Tue, 28 May 2002 11:06:06 +0200 paulson conversion of IntDiv.thy to Isar format
Fri, 17 May 2002 15:40:59 +0200 nipkow Turned into Isar theories.
Wed, 15 May 2002 13:49:51 +0200 nipkow Divides.ML -> Divides_lemmas.ML
Fri, 10 May 2002 17:59:55 +0200 nipkow *** empty log message ***
Fri, 10 May 2002 11:55:45 +0200 nipkow added dep on IMP/Compiler0
Wed, 08 May 2002 09:14:56 +0200 paulson some ex files converted to Isar
Thu, 04 Apr 2002 17:32:52 +0200 paulson conversion of Induct/{Slist,Sexp} to Isar scripts
Tue, 02 Apr 2002 14:28:28 +0200 paulson conversion of some HOL/Induct proof scripts to Isar
Thu, 14 Mar 2002 16:48:54 +0100 paulson removed ex/set.ML
Wed, 06 Mar 2002 17:56:02 +0100 wenzelm tuned;
Wed, 06 Mar 2002 17:47:51 +0100 wenzelm added HOL-Hyperreal-ex;
Tue, 05 Mar 2002 17:09:15 +0100 prensani Target HoareParallel in IsaMakefile
Sat, 02 Mar 2002 00:28:55 +0100 wenzelm temporarily disabled HoareParallel target;
Fri, 01 Mar 2002 16:24:43 +0100 prensani Completed annonce of HoareParallel
Tue, 26 Feb 2002 15:45:32 +0100 kleing introduces SystemClasses and BVExample
Tue, 26 Feb 2002 00:24:37 +0100 wenzelm Isar_examples/W_correct moved to W0;
Thu, 21 Feb 2002 20:08:09 +0100 wenzelm theory Option has been assimilated by Datatype;
Thu, 21 Feb 2002 14:08:09 +0100 kleing new MicroJava document
Sat, 16 Feb 2002 20:59:34 +0100 wenzelm converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
Tue, 05 Feb 2002 23:18:08 +0100 wenzelm moved SVC stuff to ex;
less more (0) -300 -100 -60 tip