src/HOL/Rat.thy
Fri, 14 Jun 2019 08:34:27 +0000 haftmann avoid pseudo-collection to be used in generated proofs
Fri, 14 Jun 2019 08:34:27 +0000 haftmann moved comment to approproiate place
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 29 Jun 2018 22:14:33 +0200 wenzelm merged;
Thu, 28 Jun 2018 21:05:56 +0200 wenzelm avoid pending shyps in global theory facts;
Thu, 28 Jun 2018 17:14:52 +0200 nipkow added lemmas
Thu, 14 Jun 2018 10:51:12 +0200 nipkow removed duplicates
Sat, 11 Nov 2017 18:41:08 +0000 haftmann dedicated definition for coprimality
Sun, 08 Oct 2017 22:28:21 +0200 haftmann abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
Sat, 22 Apr 2017 22:01:35 +0200 wenzelm theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
Mon, 09 Jan 2017 18:53:20 +0100 haftmann moved some lemmas to appropriate places
Tue, 03 Jan 2017 16:48:49 +0000 paulson A few new lemmas and needed adaptations
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Sun, 16 Oct 2016 09:31:04 +0200 haftmann more standardized names
Sun, 18 Sep 2016 16:59:15 +0200 wenzelm tuned proofs;
Wed, 17 Aug 2016 10:23:49 +0200 boehmes more complete simpset for linear arithmetic to avoid warnings: terms such as (2x + 2y)/2 can then be simplified by the linear arithmetic prover during its proof replay
Fri, 15 Jul 2016 12:24:04 +0200 eberlm Merged
Thu, 14 Jul 2016 14:43:09 +0200 eberlm Tuned looping simp rules in semiring_div
Fri, 15 Jul 2016 11:07:51 +0200 wenzelm misc tuning and modernization;
Mon, 20 Jun 2016 22:30:23 +0200 wenzelm misc tuning and modernization;
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Wed, 17 Feb 2016 21:51:57 +0100 haftmann dropped various legacy fact bindings
Wed, 06 Jan 2016 13:04:30 +0100 blanchet more complete setup for 'Rat' in Nitpick
Mon, 28 Dec 2015 01:26:34 +0100 wenzelm prefer symbols for "abs";
Sun, 27 Dec 2015 21:46:36 +0100 wenzelm prefer symbols for "floor", "ceiling";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 09 Sep 2015 20:57:21 +0200 wenzelm simplified simproc programming interfaces;
Mon, 31 Aug 2015 21:28:08 +0200 wenzelm prefer symbols;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Wed, 08 Jul 2015 14:01:41 +0200 haftmann avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
Fri, 12 Jun 2015 08:53:23 +0200 haftmann uniform _ div _ as infix syntax for ring division
Mon, 01 Jun 2015 18:59:21 +0200 haftmann separate class for division operator, with particular syntax added in more specific classes
Thu, 09 Apr 2015 09:12:47 +0200 haftmann conversion between division on nat/int and division in archmedean fields
Tue, 31 Mar 2015 21:54:32 +0200 haftmann given up separate type classes demanding `inverse 0 = 0`
Tue, 10 Mar 2015 15:20:40 +0000 paulson Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 30 Oct 2014 21:02:01 +0100 haftmann more simp rules concerning dvd and even/odd
Sun, 21 Sep 2014 16:56:11 +0200 haftmann explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
Sat, 19 Jul 2014 18:30:42 +0200 haftmann more appropriate postprocessing of rational numbers: extract sign to front of fraction
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Wed, 18 Jun 2014 07:31:12 +0200 hoelzl moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
Fri, 30 May 2014 18:13:40 +0200 nipkow must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
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
less more (0) -100 -60 tip