src/HOL/ex/Execute_Choice.thy
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Sat, 26 Dec 2015 15:59:27 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 06 Oct 2015 17:47:28 +0200 wenzelm isabelle update_cartouches;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 18 Oct 2012 15:52:33 +0200 kuncar update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
Mon, 12 Sep 2011 12:33:37 +0200 bulwahn correcting imports after splitting and renaming AssocList
Fri, 12 Aug 2011 14:45:50 -0700 huffman make more HOL theories work with separate set type
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Mon, 28 Jun 2010 15:32:06 +0200 haftmann dropped ancient infix mem; refined code generation operations in List.thy
Fri, 21 May 2010 17:16:16 +0200 haftmann adjusted to changes in Mapping.thy
Sun, 11 Apr 2010 16:51:05 +0200 haftmann constructor Mapping replaces AList
Wed, 17 Feb 2010 11:21:47 +0100 haftmann example for executable choice
Wed, 17 Feb 2010 09:48:53 +0100 haftmann a draft for an example how to turn specifications involving choice executable
less more (0) tip