src/HOL/ex/Execute_Choice.thy
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