isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip

move take-proofs stuff into new theory Domain_Aux.thy
2010-03-08, by huffman
add type take_info
2010-03-08, by huffman
add function add_qualified_def
2010-03-08, by huffman
merged
2010-03-08, by haftmann
proper ML interface; further polishing
2010-03-08, by haftmann
code simplification and tuning
2010-03-08, by haftmann
Added inducts field to inductive_result.
2010-03-08, by berghofe
transfer: avoid camel case, more standard coding conventions, misc tuning
2010-03-08, by haftmann
transfer: avoid camel case
2010-03-08, by haftmann
merged
2010-03-07, by huffman
generate separate qualified theorem name for each type's reach and take_lemma
2010-03-07, by huffman
add simp rule LAM_strict
2010-03-07, by huffman
fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'
2010-03-07, by huffman
merged
2010-03-07, by haftmann
dropped dead code; adhere more closely to standard coding conventions
2010-03-07, by haftmann
merged
2010-03-07, by huffman
arith tactic uses 'priority' instead of 'warning' to print messages
2010-03-07, by huffman
add simp rules about Ints, Nats
2010-03-07, by huffman
add more simp rules for Ints
2010-03-07, by huffman
add lemmas Nats_cases and Nats_induct
2010-03-07, by huffman
generalize some lemmas, and remove a few unnecessary ones
2010-03-07, by huffman
generalize some lemmas from class linordered_ring_strict to linordered_ring
2010-03-06, by huffman
add case_names attribute to casedist and ind rules
2010-03-06, by huffman
add some lemmas about complete lattices
2010-03-06, by huffman

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle