src/HOL/Algebra/Ring.thy
Wed, 24 Aug 2022 08:22:13 +0000 haftmann avoid duplicate fact error on global_interpretation of residues
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);
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Thu, 08 Nov 2018 22:29:09 +0100 wenzelm isabelle update_cartouches -t;
Sun, 22 Jul 2018 13:29:24 +0200 paulson de-applying
Tue, 03 Jul 2018 11:00:37 +0200 wenzelm more standard headers;
Sat, 30 Jun 2018 18:58:13 +0100 paulson credits to Paulo and Martin
Sat, 30 Jun 2018 15:44:04 +0100 paulson More on Algebra by Paulo and Martin
Tue, 26 Jun 2018 20:48:49 +0100 paulson a few new lemmas
Thu, 14 Jun 2018 14:23:38 +0100 paulson reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
Tue, 12 Jun 2018 16:08:57 +0100 paulson New material from Martin Baillon and Paulo Emílio de Vilhena
Wed, 06 Jun 2018 14:25:53 +0100 paulson resolution of name clashes in Algebra
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Wed, 10 Jan 2018 15:21:49 +0100 nipkow Manual updates towards conversion of "op" syntax
Fri, 05 Jan 2018 18:41:42 +0100 nipkow Renamed (^) to [^] in preparation of the move from "op X" to (X)
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Fri, 08 Jan 2016 19:46:30 +0100 wenzelm tuned;
Mon, 09 Nov 2015 15:48:17 +0100 wenzelm qualifier is mandatory by default;
Wed, 04 Nov 2015 08:13:52 +0100 ballarin Keyword 'rewrites' identifies rewrite morphisms.
Wed, 04 Nov 2015 08:13:49 +0100 ballarin Qualifiers in locale expressions default to mandatory regardless of the command.
Sat, 10 Oct 2015 19:22:05 +0200 wenzelm prefer symbols;
Sat, 10 Oct 2015 16:26:23 +0200 wenzelm isabelle update_cartouches;
Thu, 23 Jul 2015 22:13:42 +0200 wenzelm more symbols by default, without xsymbols mode;
Fri, 17 Apr 2015 11:52:36 +0200 Rene Thiemann finprod takes 1 in case of infinite sets => remove several "finite A" assumptions
Mon, 30 Mar 2015 10:58:08 +0200 Rene Thiemann added locale for semirings
Wed, 29 Oct 2014 10:58:41 +0100 wenzelm modernized setup;
Wed, 05 Mar 2014 21:51:30 +0100 wenzelm more symbols;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
less more (0) -50 -30 tip