src/HOL/Rat.thy
Fri, 08 Apr 2011 16:31:14 +0200 bulwahn rational and real instances for new compilation scheme for exhaustive quickcheck
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn moving exhaustive_generators.ML to Quickcheck directory
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Fri, 17 Dec 2010 12:14:18 +0100 bulwahn adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
Tue, 30 Nov 2010 15:58:09 +0100 haftmann adapted proofs to slightly changed definitions of congruent(2)
Mon, 29 Nov 2010 22:32:06 +0100 haftmann replaced slightly odd locale congruent by plain definition
Mon, 29 Nov 2010 13:44:54 +0100 haftmann equivI has replaced equiv.intro
Fri, 01 Oct 2010 16:05:25 +0200 haftmann constant `contents` renamed to `the_elem`
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Mon, 09 Aug 2010 12:53:16 +0200 blanchet replace "setup" with "declaration"
Fri, 06 Aug 2010 17:23:11 +0200 blanchet adapt occurrences of renamed Nitpick functions
Fri, 09 Jul 2010 08:11:10 +0200 haftmann nicer xsymbol syntax for fcomp and scomp
Fri, 11 Jun 2010 17:05:11 +0200 blanchet adjust Nitpick's handling of "<" on "rat"s and "reals"
Thu, 27 May 2010 15:15:20 +0200 wenzelm constant Rat.normalize needs to be qualified;
Tue, 27 Apr 2010 09:49:40 +0200 haftmann explicit is better than implicit
Mon, 26 Apr 2010 15:37:50 +0200 haftmann use new classes (linordered_)field_inverse_zero
Mon, 26 Apr 2010 11:34:17 +0200 haftmann class division_ring_inverse_zero
Fri, 23 Apr 2010 15:18:00 +0200 haftmann separated instantiation of division_by_zero
Sun, 11 Apr 2010 16:51:07 +0200 haftmann user interface for abstract datatypes is an attribute, not a command
Thu, 11 Mar 2010 14:39:58 +0100 haftmann tuned prefixes of ac interpretations
Sat, 27 Feb 2010 20:57:08 +0100 wenzelm clarified @{const_name} vs. @{const_abbrev};
Fri, 26 Feb 2010 10:57:35 +0100 haftmann merged
Fri, 26 Feb 2010 10:48:20 +0100 haftmann implement quotient_of for odl SML code generator
Wed, 24 Feb 2010 14:42:28 +0100 haftmann bound argument for abstype proposition
Wed, 24 Feb 2010 14:34:40 +0100 haftmann renamed theory Rational to Rat
less more (0) tip