src/HOL/Decision_Procs/Commutative_Ring.thy
Fri, 05 Jan 2018 18:41:42 +0100 nipkow Renamed (^) to [^] in preparation of the move from "op X" to (X)
Sun, 03 Dec 2017 22:28:19 +0100 wenzelm misc tuning and modernization;
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Wed, 22 Feb 2017 20:34:24 +0100 haftmann explicit dynamic context for gap-bridging function
Tue, 07 Feb 2017 22:15:07 +0100 haftmann elaborated examples for computations
Sun, 29 Jan 2017 11:59:48 +0100 berghofe Added new / improved tactics for fields and rings
Thu, 09 Jul 2015 23:46:21 +0200 wenzelm tuned proofs;
Sat, 20 Jun 2015 16:42:15 +0200 wenzelm tuned proofs;
Sat, 20 Jun 2015 16:31:44 +0200 wenzelm isabelle update_cartouches;
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
Thu, 23 Oct 2014 14:04:05 +0200 haftmann downshift of theory Parity in the hierarchy
Mon, 20 Oct 2014 12:26:44 +0200 haftmann avoid unsafe simp rules
Mon, 20 Oct 2014 07:45:58 +0200 haftmann augmented and tuned facts on even/odd and division
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Tue, 09 Sep 2014 20:51:36 +0200 blanchet ported Decision_Procs to new datatypes
Tue, 09 Sep 2014 20:51:36 +0200 blanchet use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
Thu, 27 Feb 2014 21:31:58 +0100 wenzelm tuned whitespace;
Tue, 25 Feb 2014 23:12:48 +0100 wenzelm tuned specifications and proofs;
Sun, 18 Aug 2013 19:59:19 +0200 wenzelm more symbols;
Mon, 15 Jul 2013 11:29:19 +0200 wenzelm tuned specifications and proofs;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 12 Apr 2012 18:39:19 +0200 wenzelm more standard method setup;
Mon, 21 Feb 2011 23:47:19 +0100 wenzelm tuned proofs -- eliminated prems;
Sun, 24 Oct 2010 20:19:00 +0200 nipkow nat_number -> eval_nat_numeral
Fri, 30 Oct 2009 13:59:49 +0100 haftmann moved Commutative_Ring into session Decision_Procs
less more (0) tip