isabelle: Changelog

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

isabelle