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

typedecl: no sort constraints;
2010-03-18, by wenzelm
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
2010-03-18, by wenzelm
Added product measure space
2010-03-16, by hoelzl
added type constraints to make SML/NJ happy
2010-03-18, by blanchet
merged
2010-03-18, by blanchet
fix Mirabelle after renaming Sledgehammer structures
2010-03-18, by blanchet
merged
2010-03-18, by blanchet
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-18, by blanchet
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

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

isabelle