src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
Mon, 09 Jan 2017 19:13:49 +0100 haftmann gcd/lcm on finite sets
Wed, 04 Jan 2017 21:28:29 +0100 haftmann reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
Thu, 29 Sep 2016 16:49:42 +0200 eberlm Set_Permutations replaced by more general Multiset_Permutations
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Tue, 24 May 2016 18:48:01 +0200 eberlm Removed problematic code equation for set_permutations
Tue, 24 May 2016 18:46:51 +0200 eberlm Backed out changeset 8230358fab88
Tue, 24 May 2016 17:42:14 +0200 eberlm Deleted problematic code equation in Codegenerator_Test
Fri, 26 Feb 2016 22:15:09 +0100 Manuel Eberl Tuned Euclidean Rings/GCD rings
Sun, 29 Mar 2015 19:32:27 +0200 wenzelm tuned;
Thu, 05 Feb 2015 19:44:14 +0100 haftmann slightly more standard code setup for String.literal, with explicit special case in predicate compiler
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Fri, 15 Nov 2013 22:02:01 +0100 haftmann proper code equations for Gcd and Lcm on nat and int
Sun, 10 Nov 2013 15:05:06 +0100 haftmann qualifed popular user space names
Mon, 02 Sep 2013 16:28:11 +0200 Andreas Lochbihler move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
Wed, 03 Apr 2013 22:26:04 +0200 haftmann optionalized very specific code setup for multisets
Fri, 15 Feb 2013 11:47:34 +0100 haftmann attempt to re-establish conventions which theories are loaded into the grand unified library theory;
less more (0) tip