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 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

renamed "ATP_Linkup" theory to "Sledgehammer"
2010-03-17, by blanchet
renamed Sledgehammer structures
2010-03-17, by blanchet
move Sledgehammer files in a directory of their own
2010-03-17, by blanchet
merged
2010-03-18, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-18, by haftmann
lemma swap_inj_on, swap_product
2010-03-18, by haftmann
meaningful transfer certificate
2010-03-18, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add; consider Min.insert_idem as default simp rule
2010-03-18, by haftmann
updated certificate
2010-03-18, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-18, by haftmann
added locales folding_one_(idem); various streamlining and tuning
2010-03-18, by haftmann
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-18, by haftmann
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
2010-03-17, by boehmes
added one-entry cache around Kodkod invocation
2010-03-17, by blanchet
merged
2010-03-17, by blanchet
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
2010-03-17, by blanchet
minor additions to Nitpick docs
2010-03-17, by blanchet
NEWS: Nat_Bijection library
2010-03-17, by huffman
document "nitpick_choice_spec" attribute
2010-03-17, by blanchet
fix typo in "nitpick_choice_spec" attribute name (singular, not plural)
2010-03-17, by blanchet
added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-17, by blanchet
rollback of local typedef until problem with type-variables can be sorted out; fixed header
2010-03-16, by Christian Urban
adjusted to changes in Finite_Set
2010-03-16, by haftmann
merged
2010-03-15, by wenzelm
merged
2010-03-15, by nipkow
tuned inductions
2010-03-15, by nipkow
tuned;
2010-03-15, by wenzelm
moved old Sign.intern_term to the place where it is still used;
2010-03-15, by wenzelm
preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
2010-03-15, by wenzelm
replaced type_syntax/term_syntax by uniform syntax_declaration;
2010-03-15, by wenzelm
merged
2010-03-15, by haftmann
corrected disastrous syntax declarations
2010-03-15, by haftmann
added stmaryrd for isasymSqinter
2010-03-15, by haftmann
use headers consistently
2010-03-14, by huffman
no_document for theory Countable
2010-03-14, by huffman
old domain package also defines map functions
2010-03-14, by huffman
separate map-related code into new function define_map_functions
2010-03-14, by huffman
removed Local_Theory.theory_result by using local Typedef.add_typedef
2010-03-14, by Christian Urban
tuned comment;
2010-03-14, by wenzelm
observe standard header format;
2010-03-14, by wenzelm
expose formal text;
2010-03-14, by wenzelm
localized @{class} and @{type};
2010-03-14, by wenzelm
move functions into holcf_library.ML
2010-03-14, by huffman
simplify definition of when combinators
2010-03-14, by huffman
declare case_names for various induction rules
2010-03-13, by huffman
add case name 'adm' for infinite induction rules
2010-03-13, by huffman
renamed some lemmas generated by the domain package
2010-03-13, by huffman
use Simplifier.context to avoid 'no proof context in simpset' errors from fixrec_simp after theory merge
2010-03-13, by huffman
fixpat command prints legacy_feature warning
2010-03-13, by huffman
merged
2010-03-13, by huffman
pass binding as argument to add_domain_constructors; proper binding for case combinator
2010-03-13, by huffman
pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names
2010-03-13, by huffman
pass take_info as argument to Domain_Theorems.theorems
2010-03-13, by huffman
replace some string arguments with bindings
2010-03-13, by huffman
more consistent use of qualified bindings
2010-03-13, by huffman
avoid unnecessary primed variable names
2010-03-13, by huffman
remove redundant lemmas
2010-03-13, by huffman
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
2010-03-13, by huffman
fixrec now generates qualified theorem names
2010-03-13, by huffman
no_document for Infinite_Set in HOLCF
2010-03-13, by huffman

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

isabelle