| Tue, 02 Mar 2010 13:50:23 -0800 | huffman | move take-related definitions and proofs to new module; simplify map_of_typ functions | changeset | files |
| Tue, 02 Mar 2010 13:01:22 -0800 | huffman | remove map_tab argument to calc_axioms | changeset | files |
| Tue, 02 Mar 2010 09:54:50 -0800 | huffman | remove dead code | changeset | files |
| Tue, 02 Mar 2010 17:36:40 +0000 | paulson | merged | changeset | files |
| Tue, 02 Mar 2010 17:36:16 +0000 | paulson | Slightly generalised a theorem | changeset | files |
| Tue, 02 Mar 2010 12:59:16 +0000 | paulson | merged | changeset | files |
| Fri, 19 Feb 2010 16:52:11 +0000 | paulson | merged | changeset | files |
| Fri, 19 Feb 2010 15:21:57 +0000 | paulson | merged | changeset | files |
| Fri, 05 Feb 2010 17:19:25 +0000 | paulson | merged | changeset | files |
| Thu, 04 Feb 2010 11:33:54 +0000 | paulson | merged | changeset | files |
| Tue, 02 Feb 2010 09:49:07 +0000 | paulson | merged | changeset | files |
| Tue, 02 Feb 2010 09:48:20 +0000 | paulson | Correction of a tiny error | changeset | files |
| Tue, 02 Mar 2010 17:45:10 +0100 | krauss | removed obsolete helper theory | changeset | files |
| Tue, 02 Mar 2010 15:39:15 +0100 | haftmann | merged | changeset | files |
| Tue, 02 Mar 2010 15:39:06 +0100 | haftmann | dropped superfluous naming | changeset | files |
| Tue, 02 Mar 2010 04:53:18 -0800 | huffman | UNIV is not a logical constant | changeset | files |
| Tue, 02 Mar 2010 04:35:44 -0800 | huffman | merged | changeset | files |
| Tue, 02 Mar 2010 04:31:50 -0800 | huffman | re-enable bisim code, now in domain_theorems.ML | changeset | files |
| Tue, 02 Mar 2010 04:19:06 -0800 | huffman | add missing rule to case_strict proof script | changeset | files |
| Tue, 02 Mar 2010 02:28:45 -0800 | huffman | remove dead code | changeset | files |
| Tue, 02 Mar 2010 00:34:26 -0800 | huffman | domain package no longer generates copy functions; all proofs use take functions instead | changeset | files |
| Mon, 01 Mar 2010 23:54:50 -0800 | huffman | need to explicitly include REP_convex | changeset | files |
| Mon, 01 Mar 2010 19:18:08 -0800 | huffman | add lemma lub_eq | changeset | files |
| Mon, 01 Mar 2010 17:32:23 -0800 | huffman | add lemmas about ssum_map and sprod_map | changeset | files |
| Mon, 01 Mar 2010 16:58:16 -0800 | huffman | generate take_take rules | changeset | files |
| Mon, 01 Mar 2010 16:36:25 -0800 | huffman | add function define_take_functions | changeset | files |
| Mon, 01 Mar 2010 11:15:18 -0800 | huffman | add missing strictify rule to proof script | changeset | files |
| Mon, 01 Mar 2010 10:00:14 -0800 | huffman | qualify constructor names with type name | changeset | files |
| Mon, 01 Mar 2010 09:55:32 -0800 | huffman | move definition of case combinator to domain_constructors.ML | changeset | files |
| Mon, 01 Mar 2010 08:33:49 -0800 | huffman | remove dependence on Domain_Library | changeset | files |