src/HOL/Import/HOL_Light_Maps.thy
Wed, 23 Jun 2021 17:43:31 +0000 haftmann more default simp rules
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Mon, 26 Sep 2016 07:56:54 +0200 haftmann syntactic type class for operation mod named after mod;
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Fri, 12 Jun 2015 08:53:23 +0200 haftmann uniform _ div _ as infix syntax for ring division
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 23 Oct 2014 14:43:51 +0200 haftmann explicit definition restores HOL Light import after cb9d84d3e7f2
Mon, 24 Mar 2014 16:06:55 +0100 wenzelm formal check of user input, avoiding direct references of interal names;
Sun, 16 Feb 2014 21:33:28 +0100 blanchet folded 'list_all2' with the relator generated by 'datatype_new'
Fri, 14 Feb 2014 07:53:46 +0100 blanchet merged 'Option.map' and 'Option.map_option'
Wed, 12 Feb 2014 08:37:06 +0100 blanchet adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet adapted theories to '{case,rec}_{list,option}' names
Wed, 12 Feb 2014 08:35:56 +0100 blanchet se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
Wed, 25 Dec 2013 17:39:06 +0100 haftmann prefer more canonical names for lemmas on min/max
Wed, 04 Apr 2012 20:10:21 +0200 Cezary Kaliszyk HOL/Import more precise map types
Sun, 01 Apr 2012 14:50:47 +0200 Cezary Kaliszyk Modernized HOL-Import for HOL Light
less more (0) tip