src/HOL/RealDef.thy
Wed, 23 Sep 2009 14:00:12 +0200 Code_Eval(uation)
Tue, 14 Jul 2009 16:27:32 +0200 prefer code_inline over code_unfold; use code_unfold_post where appropriate
Tue, 14 Jul 2009 10:54:04 +0200 code attributes use common underscore convention
Tue, 07 Jul 2009 17:39:51 +0200 renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
Wed, 17 Jun 2009 16:56:15 -0700 merged
Wed, 17 Jun 2009 16:55:01 -0700 new GCD library, courtesy of Jeremy Avigad
Tue, 16 Jun 2009 16:26:40 +0200 denominator should not be zero
Mon, 15 Jun 2009 16:13:03 +0200 hide constant Quickcheck.random
Tue, 19 May 2009 13:57:32 +0200 moved Code_Index, Random and Quickcheck before Main
Mon, 11 May 2009 15:18:32 +0200 tuned interface of Lin_Arith
Wed, 04 Mar 2009 11:05:29 +0100 Merge.
Wed, 04 Mar 2009 10:45:52 +0100 Merge.
Mon, 02 Mar 2009 16:53:55 +0100 name changes
Tue, 24 Feb 2009 11:12:58 -0800 make more proofs work whether or not One_nat_def is a simp rule
Sat, 21 Feb 2009 20:52:30 +0100 Removed subsumed lemmas
Wed, 28 Jan 2009 16:29:16 +0100 Replaced group_ and ring_simps by algebra_simps;
Wed, 03 Dec 2008 15:58:44 +0100 made repository layout more coherent with logical distribution structure; stripped some $Id$s