Wed, 11 Feb 2009 23:05:58 +1100 kleing updated NEWS etc with "solves" criterion and auto_solves
Wed, 11 Feb 2009 10:51:31 +0100 nipkow merged
Wed, 11 Feb 2009 10:51:07 +0100 nipkow Moved Order_Relation into Library and moved some of it into Relation.
Wed, 11 Feb 2009 16:03:10 +1100 kleing Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
Wed, 11 Feb 2009 14:48:14 +1100 kleing FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
Tue, 10 Feb 2009 17:53:51 -0800 huffman const_name antiquotations
Tue, 10 Feb 2009 10:25:09 +0000 paulson Repaired a proof that did, after all, refer to the theorem nat_induct2.
Tue, 10 Feb 2009 09:58:58 +0000 paulson merged
Tue, 10 Feb 2009 09:51:23 +0000 paulson Strengthened the induction rule nat_induct2.
Tue, 10 Feb 2009 09:46:11 +0000 paulson Deleted the induction rule nat_induct2, which was too weak and not used even once.
Mon, 09 Feb 2009 22:15:37 +0100 nipkow merged
Mon, 09 Feb 2009 22:14:33 +0100 nipkow fix to [arith]
Mon, 09 Feb 2009 18:50:10 +0100 nipkow new attribute "arith" for facts supplied to arith.
Mon, 09 Feb 2009 17:25:07 +1100 Timothy Bourke Nicer names in FindTheorems.
Mon, 09 Feb 2009 17:21:46 +0000 chaieb added Determinants to Library
Mon, 09 Feb 2009 17:21:19 +0000 chaieb Traces, Determinant of square matrices and some properties
Mon, 09 Feb 2009 17:09:18 +0000 chaieb added Euclidean_Space and Glbs to Library
Mon, 09 Feb 2009 17:08:49 +0000 chaieb fixed proof -- removed unnecessary sorry
Mon, 09 Feb 2009 16:57:10 +0000 chaieb Fixed theorem reference
Mon, 09 Feb 2009 16:54:03 +0000 chaieb (Real) Vectors in Euclidean space, and elementary linear algebra.
Mon, 09 Feb 2009 16:43:52 +0000 chaieb A generic decision procedure for linear rea arithmetic and normed vector spaces
Mon, 09 Feb 2009 16:42:15 +0000 chaieb Permutations, both general and specifically on finite sets.
Mon, 09 Feb 2009 16:20:24 +0000 chaieb Imports Main in order to avoid the typerep problem
Mon, 09 Feb 2009 16:19:46 +0000 chaieb A theory of greatest lower bounds
Mon, 09 Feb 2009 15:38:26 +0000 chaieb Now imports Fact as suggested by Florian in order to avoid the typerep problem
Mon, 09 Feb 2009 11:15:13 +0000 chaieb Added HOL/Library/Finite_Cartesian_Product.thy to Library
Mon, 09 Feb 2009 11:07:17 +0000 chaieb A formalization of finite cartesian product types
Mon, 09 Feb 2009 11:19:44 +0100 hoelzl Proof method 'reify' is now reentrant.
Sun, 08 Feb 2009 11:59:26 +0100 nipkow added noatps
Sat, 07 Feb 2009 10:56:44 +0100 haftmann check for destination directory, do not allocate it gratuitously
Sat, 07 Feb 2009 10:03:09 +0100 haftmann Isar proof
Sat, 07 Feb 2009 09:58:24 +0100 haftmann merged
Sat, 07 Feb 2009 09:57:07 +0100 haftmann code theorems for nth, list_update
Sat, 07 Feb 2009 09:57:03 +0100 haftmann added bulkload
Sat, 07 Feb 2009 08:37:43 +0100 haftmann code theorems for nth, list_update
Sat, 07 Feb 2009 08:37:42 +0100 haftmann added bulkload
Sat, 07 Feb 2009 09:25:59 +0100 haftmann added Decision_Procs.thy
Fri, 06 Feb 2009 15:15:46 +0100 haftmann merged
Fri, 06 Feb 2009 15:15:32 +0100 haftmann session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
Fri, 06 Feb 2009 15:15:27 +0100 haftmann authentic syntax for List.nth
Fri, 06 Feb 2009 14:36:58 +0100 berghofe Merged.
Fri, 06 Feb 2009 13:43:19 +0100 blanchet Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
Fri, 06 Feb 2009 08:23:15 +0000 chaieb Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
Fri, 06 Feb 2009 08:22:32 +0000 chaieb fixed import
Fri, 06 Feb 2009 09:06:17 +0100 haftmann merged
Fri, 06 Feb 2009 09:05:20 +0100 haftmann more robust failure in error situations
Fri, 06 Feb 2009 09:05:19 +0100 haftmann mandatory prefix for index conversion operations
Fri, 06 Feb 2009 09:05:19 +0100 haftmann added replace operation
Fri, 06 Feb 2009 00:13:15 +0000 chaieb fixed dependencies : Theory Dense_Linear_Order moved to Library
Fri, 06 Feb 2009 00:10:58 +0000 chaieb Theory Dense_Linear_Order moved to Library
Fri, 06 Feb 2009 00:10:58 +0000 chaieb fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
Thu, 05 Feb 2009 15:35:06 +0100 hoelzl Updated NEWS about approximation
Thu, 05 Feb 2009 14:50:43 +0100 haftmann merged
Thu, 05 Feb 2009 14:14:03 +0100 haftmann split of already properly working part of Quickcheck infrastructure
Thu, 05 Feb 2009 14:14:03 +0100 haftmann code attribute applied before user attributes
Thu, 05 Feb 2009 14:14:02 +0100 haftmann moved Random.thy to Library
Thu, 05 Feb 2009 11:49:15 +0100 hoelzl Add approximation method
Thu, 05 Feb 2009 11:45:15 +0100 hoelzl Added new Float theory and moved old Library/Float.thy to ComputeFloat
Thu, 05 Feb 2009 11:34:42 +0100 hoelzl Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
Wed, 04 Feb 2009 18:10:07 +0100 blanchet Make some Refute functions public so I can use them in Nitpick,
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip