paulson [Tue, 02 Feb 2010 09:49:07 +0000] rev 35504
merged
paulson [Tue, 02 Feb 2010 09:48:20 +0000] rev 35503
Correction of a tiny error
krauss [Tue, 02 Mar 2010 17:45:10 +0100] rev 35502
removed obsolete helper theory
haftmann [Tue, 02 Mar 2010 15:39:15 +0100] rev 35501
merged
haftmann [Tue, 02 Mar 2010 15:39:06 +0100] rev 35500
dropped superfluous naming
huffman [Tue, 02 Mar 2010 04:53:18 -0800] rev 35499
UNIV is not a logical constant
huffman [Tue, 02 Mar 2010 04:35:44 -0800] rev 35498
merged
huffman [Tue, 02 Mar 2010 04:31:50 -0800] rev 35497
re-enable bisim code, now in domain_theorems.ML
huffman [Tue, 02 Mar 2010 04:19:06 -0800] rev 35496
add missing rule to case_strict proof script
huffman [Tue, 02 Mar 2010 02:28:45 -0800] rev 35495
remove dead code
huffman [Tue, 02 Mar 2010 00:34:26 -0800] rev 35494
domain package no longer generates copy functions; all proofs use take functions instead
huffman [Mon, 01 Mar 2010 23:54:50 -0800] rev 35493
need to explicitly include REP_convex
huffman [Mon, 01 Mar 2010 19:18:08 -0800] rev 35492
add lemma lub_eq
huffman [Mon, 01 Mar 2010 17:32:23 -0800] rev 35491
add lemmas about ssum_map and sprod_map
huffman [Mon, 01 Mar 2010 16:58:16 -0800] rev 35490
generate take_take rules
huffman [Mon, 01 Mar 2010 16:36:25 -0800] rev 35489
add function define_take_functions