src/HOL/MicroJava/BV/BVExample.thy
Mon, 29 Jun 2009 12:18:57 +0200 haftmann explicit Set constructor for code generated for sets
Mon, 18 May 2009 23:15:38 +0200 nipkow fine-tuned elimination of comprehensions involving x=t.
Sat, 16 May 2009 17:44:11 +0200 nipkow proof tuned
Sat, 16 May 2009 11:28:02 +0200 nipkow "{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
Tue, 07 Oct 2008 16:07:25 +0200 haftmann tuned code setup
Mon, 20 Aug 2007 18:54:51 +0200 wenzelm theory header: fixed import;
Mon, 20 Aug 2007 17:46:31 +0200 wenzelm theory header: more precise imports;
less more (0) -30 -10 -7 tip