Sat, 16 Oct 2010 17:09:57 -0700 | huffman | remove old uses of 'simp_tac HOLCF_ss' | changeset | files |
Sat, 16 Oct 2010 16:39:06 -0700 | huffman | merged | changeset | files |
Sat, 16 Oct 2010 16:22:42 -0700 | huffman | remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check | changeset | files |
Sat, 16 Oct 2010 15:26:30 -0700 | huffman | reimplement proof automation for coinduct rules | changeset | files |