2010-03-08 | huffman | generate take_induct lemmas | file | diff | annotate |
2010-03-08 | huffman | move lemmas from Domain.thy to Domain_Aux.thy | file | diff | annotate |
2010-03-08 | huffman | move take-proofs stuff into new theory Domain_Aux.thy | file | diff | annotate |