src/HOL/Algebra/Divisibility.thy
Mon, 17 May 2021 09:07:30 +0000 haftmann mere abbreviation for logical alias
Thu, 25 Mar 2021 08:52:15 +0000 haftmann dedicated session for combinatorial material
Sat, 06 Mar 2021 18:42:10 +0000 haftmann consolidated names
Tue, 02 Mar 2021 08:09:05 +0000 haftmann reduced dependencies on theory List_Permutation
Tue, 23 Feb 2021 20:41:48 +0000 haftmann more specific name
Tue, 30 Apr 2019 11:57:45 +0100 paulson Algebraic closure: moving more theorems into their rightful places
Mon, 29 Apr 2019 17:11:26 +0100 paulson moving around some material from Algebraic_Closure
Sun, 10 Mar 2019 23:23:03 +0100 wenzelm more formal contributors (with the help of the history);
Mon, 21 Jan 2019 14:44:23 +0000 paulson new material about summations and powers, along with some tweaks
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 25 Jul 2018 00:25:05 +0200 paulson de-applying
Thu, 19 Jul 2018 23:23:10 +0200 paulson updated material concerning Algebra
Sun, 08 Jul 2018 16:07:26 +0100 paulson elimination of some "smt"
Sat, 30 Jun 2018 15:44:04 +0100 paulson More on Algebra by Paulo and Martin
Sun, 24 Jun 2018 11:41:32 +0100 paulson more modernisaton and de-applying
Thu, 21 Jun 2018 23:05:32 +0100 paulson de-applying Divisibility
Wed, 20 Jun 2018 22:46:48 +0100 paulson More clear-up of Divisibility
Tue, 19 Jun 2018 23:11:00 +0100 paulson Partial de-apply of Divisibility
Wed, 06 Jun 2018 14:25:53 +0100 paulson resolution of name clashes in Algebra
Thu, 19 Apr 2018 14:49:08 +0100 paulson some simpler, cleaner proofs
Tue, 16 Jan 2018 09:30:00 +0100 wenzelm standardized towards new-style formal comments: isabelle update_comments;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sat, 06 Jan 2018 09:39:57 +0100 nipkow tuned op
Thu, 31 Aug 2017 21:48:01 +0200 ballarin Revert 5a42eddc11c1.
Thu, 24 Aug 2017 17:41:49 +0200 haftmann swapping of theory dependency yields less pervasive syntax requiring popular symbols \<mu>, \<nu>
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Sat, 17 Dec 2016 15:22:13 +0100 haftmann standardized notation
Mon, 19 Sep 2016 20:07:39 +0200 fleury # after multiset intersection and union symbol
Mon, 12 Sep 2016 00:11:20 +0200 wenzelm tuned proofs;
Sun, 11 Sep 2016 23:30:23 +0200 wenzelm tuned proofs;
Sun, 11 Sep 2016 00:13:25 +0200 wenzelm misc tuning and modernization;
Mon, 05 Sep 2016 15:47:50 +0200 fleury add_mset constructor in multisets
Mon, 08 Aug 2016 17:47:51 +0200 eberlm is_prime -> prime
Wed, 20 Jul 2016 13:51:38 +0200 fleury adding mset_map to the simp rules
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Fri, 26 Feb 2016 22:44:11 +0100 haftmann more succint formulation of membership for multisets, similar to lists;
Sat, 10 Oct 2015 16:26:23 +0200 wenzelm isabelle update_cartouches;
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Fri, 19 Jun 2015 15:55:22 +0200 nipkow renamed multiset_of -> mset
Wed, 17 Jun 2015 17:21:11 +0200 nipkow renamed Multiset.set_of to the canonical set_mset
Wed, 10 Jun 2015 13:24:16 +0200 Mathias Fleury Renaming multiset operators < ~> <#,...
Wed, 22 Apr 2015 12:11:48 +0200 nipkow added simp rules for ==>
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Tue, 09 Sep 2014 17:50:54 +0200 nipkow enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
Tue, 05 Aug 2014 16:58:19 +0200 wenzelm tuned proofs -- fewer warnings;
Wed, 11 Jun 2014 14:24:23 +1000 Thomas Sewell Hypsubst preserves equality hypotheses
Sun, 02 Feb 2014 19:15:25 +0000 paulson Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Thu, 08 Nov 2012 20:02:41 +0100 bulwahn tuned proofs
Fri, 06 Jan 2012 10:19:47 +0100 haftmann tuned proofs
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Fri, 02 Sep 2011 18:17:45 +0200 wenzelm tuned proofs;
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Thu, 13 May 2010 14:34:05 +0200 nipkow Multiset: renamed, added and tuned lemmas;
Thu, 22 Apr 2010 20:39:48 +0100 paulson Tidied up using s/l
Sun, 21 Mar 2010 17:12:31 +0100 wenzelm standard headers;
Sun, 21 Mar 2010 16:51:37 +0100 wenzelm slightly more uniform definitions -- eliminated old-style meta-equality;
Sun, 21 Mar 2010 15:57:40 +0100 wenzelm eliminated old constdefs;
less more (0) -60 tip