Mercurial
Mercurial
>
repos
>
testboard
/ 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
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.
changing more definitions to quotient_definition
20120328, by bulwahn
removing now redundant impl_of theorems in DAList
20120328, by bulwahn
using abstract code equations for proofs of code equations in Multiset
20120328, by bulwahn
simplified statements and proofs;
20120328, by wenzelm
tuned whitespace;
20120328, by wenzelm
updated Sign.add_type, Name_Space.declare;
20120328, by wenzelm
updated comments;
20120328, by wenzelm
merged
20120328, by huffman
remove unnecessary rules from the simpset
20120327, by huffman
remove unused premises
20120327, by huffman
remove duplicate lemmas
20120327, by huffman
mark some duplicate lemmas for deletion
20120327, by huffman
remove more redundant lemmas
20120327, by huffman
tuned proofs
20120327, by huffman
remove redundant lemmas
20120327, by huffman
generalized lemma zpower_zmod
20120327, by huffman
remove redundant lemma
20120327, by huffman
remove redundant lemma
20120327, by huffman
remove duplicate [algebra] declarations
20120327, by huffman
generalize more div/mod lemmas
20120327, by huffman
generalize some theorems about div/mod
20120327, by huffman
updated to jedit4.5.1;
20120328, by wenzelm
merged
20120327, by kuncar
note a code eqn in quotient_def
20120327, by kuncar
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
20120327, by boehmes
more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
20120327, by blanchet
fixed etaextension of higherorder quantifiers in THF output
20120327, by blanchet
renamed "smt_fixed" to "smt_read_only_certificates"
20120327, by blanchet
tuning
20120327, by blanchet
tuning (in particular, Symtab instead of AList)
20120327, by blanchet
tweak slices, based on eval by Daniel Wand
20120327, by blanchet
be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
20120327, by blanchet
print a hint
20120327, by blanchet
avoid DL
20120327, by blanchet
TFF: declare free types as types
20120327, by blanchet
merged
20120327, by bulwahn
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
20120327, by bulwahn
remove redundant lemmas
20120327, by huffman
move int::ring_div instance upward, simplify several proofs
20120327, by huffman
rename lemmas {divmod_int_rel_{div,mod} > {div,mod}_int_unique, for consistency with nat lemma names
20120327, by huffman
extend definition of divmod_int_rel to handle denominator=0 case
20120327, by huffman
tuned proofs
20120327, by huffman
shorten a proof
20120327, by huffman
simplify some proofs
20120327, by huffman
rename lemmas {div,mod}_eq > {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.
20120327, by huffman
simplify some proofs
20120327, by huffman
merged
20120326, by wenzelm
merged
20120326, by nipkow
reverted to canonical name
20120326, by nipkow
merged
20120326, by wenzelm
merged
20120326, by huffman
revert changeset 500a5d97511a, reenabling HOLProofsLambda
20120326, by huffman
merged
20120326, by huffman
fix incorrect code_modulename declarations
20120326, by huffman
code lemma for function 'nat' that doesn't go into an infinite loop (fixes problem with nonterminating HOLProofsLambda)
20120326, by huffman
remove oldstyle semicolon
20120326, by huffman
merged
20120326, by nipkow
Functions and lemmas by Christian Sternagel
20120326, by nipkow
more precise treatment of \r\n as blank symbol (cf. 2bf29095d26f), e.g. relevant for loading theory headers in Isabelle/jEdit  NB: jEdit and Isabelle/ML normalize newline variants to \n, but Isabelle/Scala retains them literally;
20120326, by wenzelm
disabled HOLProofsLambda temporarily, which causes problems with 2a1953f0d20d;
20120326, by wenzelm
less
more

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