src/HOL/Rat.thy
Mon, 14 Apr 2014 13:08:17 +0200 hoelzl added divide_nonneg_nonneg and co; made it a simp rule
Sat, 12 Apr 2014 17:26:27 +0200 nipkow made mult_pos_pos a simp rule
Wed, 09 Apr 2014 09:37:47 +0200 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
Thu, 03 Apr 2014 23:51:52 +0100 paulson removing simprule status for divide_minus_left and divide_minus_right
Fri, 07 Mar 2014 11:46:26 +0100 wenzelm more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;
Sat, 25 Jan 2014 22:06:07 +0100 wenzelm explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
Wed, 25 Dec 2013 17:39:06 +0100 haftmann prefer more canonical names for lemmas on min/max
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Tue, 12 Nov 2013 19:28:51 +0100 hoelzl support of_rat with 0 or 1 on order relations
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Mon, 16 Sep 2013 15:30:20 +0200 kuncar use lifting_forget for deregistering numeric types as a quotient type
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 13 Aug 2013 17:45:22 +0200 wenzelm merged
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Tue, 13 Aug 2013 15:59:22 +0200 kuncar move Lifting/Transfer relevant parts of Library/Quotient_* to Main
Sat, 25 May 2013 17:13:34 +0200 wenzelm tuned;
Mon, 13 May 2013 13:59:04 +0200 kuncar better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
Tue, 19 Feb 2013 15:03:36 +0100 kuncar delete also predicates on relations when hiding an implementation of an abstract type
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Thu, 14 Feb 2013 15:27:10 +0100 haftmann reform of predicate compiler / quickcheck theories:
Fri, 23 Nov 2012 18:28:00 +0100 hoelzl add quotient_of_div
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Mon, 21 May 2012 16:37:28 +0200 kuncar use quot_del instead of ML code in Rat.thy
Thu, 10 May 2012 21:02:36 +0200 huffman simplify instance proofs for rat
Thu, 10 May 2012 21:18:41 +0200 huffman convert Rat.thy to use lift_definition/transfer
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Fri, 02 Mar 2012 09:35:35 +0100 bulwahn choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
Mon, 12 Dec 2011 13:45:54 +0100 bulwahn hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Tue, 15 Nov 2011 15:38:50 +0100 bulwahn improved generators for rational numbers to generate negative numbers;
Sun, 13 Nov 2011 20:28:22 +0100 blanchet remove unsound line in Nitpick's "rat" setup
Wed, 19 Oct 2011 09:11:14 +0200 bulwahn removing old code generator setup for rational numbers; tuned
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn adding code equations for partial_term_of for rational numbers
Mon, 18 Jul 2011 10:34:21 +0200 bulwahn adding narrowing instances for real and rational
Sat, 09 Jul 2011 19:28:33 +0200 bulwahn adding code equations to execute floor and ceiling on rational and real numbers
Sat, 09 Jul 2011 13:41:58 +0200 bulwahn adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
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
less more (0) -60 tip