2010-03-08 huffman construct fully typed goal in proof of induction rule
2010-03-08 huffman don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
2010-03-08 huffman remove redundant function arguments
2010-03-08 huffman include take_info within take_induct_info type
2010-03-08 huffman pass take_info as an argument to comp_theorems
2010-03-08 huffman pass take_induct_info as an argument to comp_theorems
2010-03-08 huffman add type take_induct_info
2010-03-08 huffman generate take_induct lemmas
2010-03-08 huffman move proofs of reach and take lemmas to domain_take_proofs.ML
2010-03-08 huffman move lemmas from Domain.thy to Domain_Aux.thy
2010-03-08 huffman move take-proofs stuff into new theory Domain_Aux.thy
2010-03-08 huffman add type take_info
2010-03-08 huffman add function add_qualified_def
2010-03-08 haftmann merged
2010-03-08 haftmann proper ML interface; further polishing
2010-03-08 haftmann code simplification and tuning
2010-03-08 berghofe Added inducts field to inductive_result.
2010-03-08 haftmann transfer: avoid camel case, more standard coding conventions, misc tuning
2010-03-08 haftmann transfer: avoid camel case
2010-03-08 huffman merged
2010-03-08 huffman generate separate qualified theorem name for each type's reach and take_lemma
2010-03-08 huffman add simp rule LAM_strict
2010-03-07 huffman fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'
2010-03-07 haftmann merged
2010-03-07 haftmann dropped dead code; adhere more closely to standard coding conventions
2010-03-07 huffman merged
2010-03-07 huffman arith tactic uses 'priority' instead of 'warning' to print messages
2010-03-07 huffman add simp rules about Ints, Nats
Loading...
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip