src/HOL/Decision_Procs/Commutative_Ring.thy
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