Thu, 19 Nov 2009 22:25:11 -0800 | huffman | store map_ID thms in theory data; automate proofs of reach lemmas | file | diff | annotate |
Thu, 19 Nov 2009 12:38:02 -0800 | huffman | set up domain_isomorphism package in Representable.thy | file | diff | annotate |
Thu, 19 Nov 2009 10:25:17 -0800 | huffman | add lemma isodefl_cprod | file | diff | annotate |
Thu, 19 Nov 2009 08:22:00 -0800 | huffman | change naming convention for deflation combinators | file | diff | annotate |
Wed, 18 Nov 2009 16:57:58 -0800 | huffman | remove one_typ and tr_typ; add abs/rep lemmas | file | diff | annotate |
Fri, 13 Nov 2009 15:31:20 -0800 | huffman | automate definition of representable domains from algebraic deflations | file | diff | annotate |
Tue, 10 Nov 2009 06:30:08 -0800 | huffman | add title/author block | file | diff | annotate |
Tue, 10 Nov 2009 06:22:29 -0800 | huffman | theory of representable cpos | file | diff | annotate |