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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
merged
20100318, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
20100318, by haftmann
lemma swap_inj_on, swap_product
20100318, by haftmann
meaningful transfer certificate
20100318, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add; consider Min.insert_idem as default simp rule
20100318, by haftmann
updated certificate
20100318, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
20100318, by haftmann
added locales folding_one_(idem); various streamlining and tuning
20100318, by haftmann
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
20100318, by haftmann
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
20100317, by boehmes
added oneentry cache around Kodkod invocation
20100317, by blanchet
merged
20100317, by blanchet
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
20100317, by blanchet
minor additions to Nitpick docs
20100317, by blanchet
NEWS: Nat_Bijection library
20100317, by huffman
document "nitpick_choice_spec" attribute
20100317, by blanchet
fix typo in "nitpick_choice_spec" attribute name (singular, not plural)
20100317, by blanchet
added support for "specification" and "ax_specification" constructs to Nitpick
20100317, by blanchet
rollback of local typedef until problem with typevariables can be sorted out; fixed header
20100316, by Christian Urban
adjusted to changes in Finite_Set
20100316, by haftmann
merged
20100315, by wenzelm
merged
20100315, by nipkow
tuned inductions
20100315, by nipkow
tuned;
20100315, by wenzelm
moved old Sign.intern_term to the place where it is still used;
20100315, by wenzelm
preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
20100315, by wenzelm
replaced type_syntax/term_syntax by uniform syntax_declaration;
20100315, by wenzelm
merged
20100315, by haftmann
corrected disastrous syntax declarations
20100315, by haftmann
added stmaryrd for isasymSqinter
20100315, by haftmann
use headers consistently
20100314, by huffman
no_document for theory Countable
20100314, by huffman
old domain package also defines map functions
20100314, by huffman
separate maprelated code into new function define_map_functions
20100314, by huffman
removed Local_Theory.theory_result by using local Typedef.add_typedef
20100314, by Christian Urban
tuned comment;
20100314, by wenzelm
observe standard header format;
20100314, by wenzelm
expose formal text;
20100314, by wenzelm
localized @{class} and @{type};
20100314, by wenzelm
move functions into holcf_library.ML
20100314, by huffman
simplify definition of when combinators
20100314, by huffman
declare case_names for various induction rules
20100313, by huffman
add case name 'adm' for infinite induction rules
20100313, by huffman
renamed some lemmas generated by the domain package
20100313, by huffman
use Simplifier.context to avoid 'no proof context in simpset' errors from fixrec_simp after theory merge
20100313, by huffman
fixpat command prints legacy_feature warning
20100313, by huffman
merged
20100313, by huffman
pass binding as argument to add_domain_constructors; proper binding for case combinator
20100313, by huffman
pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names
20100313, by huffman
pass take_info as argument to Domain_Theorems.theorems
20100313, by huffman
replace some string arguments with bindings
20100313, by huffman
more consistent use of qualified bindings
20100313, by huffman
avoid unnecessary primed variable names
20100313, by huffman
remove redundant lemmas
20100313, by huffman
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
20100313, by huffman
fixrec now generates qualified theorem names
20100313, by huffman
no_document for Infinite_Set in HOLCF
20100313, by huffman
removed unused Args.maxidx_values and Element.generalize_facts;
20100313, by wenzelm
Local_Theory.define handles hidden polymorphism;
20100313, by wenzelm
local theory specifications handle hidden polymorphism implicitly;
20100313, by wenzelm
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip