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.
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
tuned comment
20120326, by kuncar
merged
20120326, by kuncar
merged
20120326, by kuncar
tuned proof  no smt call
20120326, by kuncar
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
20120326, by wenzelm
updated theory header syntax and related details;
20120326, by wenzelm
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
20120324, by wenzelm
merged
20120326, by wenzelm
reintroduced broken proofs and regenerated certificates
20120326, by blanchet
merged, resolving trivial conflict;
20120326, by wenzelm
fixed Nitpick after numeral representation change (2a1953f0d20d)
20120326, by blanchet
merged fork with new numeral representation (see NEWS)
20120325, by huffman
merged
20120324, by kuncar
use Thm.transfer for thms stored in generic context data storage
20120323, by kuncar
hide invariant constant
20120323, by kuncar
explicit SMTP server (appears to be required after recent change of system configuration);
20120324, by wenzelm
more isatest subscribers;
20120324, by wenzelm
merged
20120323, by paulson
proof tidying
20120323, by paulson
updated comment
20120116, by kuncar
resolve invariant constant name clash
20120323, by kuncar
update etc/isarkeywords.el
20120323, by kuncar
fix example files
20120323, by kuncar
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
20120323, by kuncar
simplified code of generation of aggregate relations
20120323, by kuncar
store the relational theorem for every relator
20120323, by kuncar
store the quotient theorem for every quotient
20120323, by kuncar
fix Quotient_Examples
20120323, by kuncar
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
20120323, by kuncar
adjusting to longer names in PNF_Narrowing_Engine, which was overlooked in 4106258260b3
20120323, by bulwahn
less
more

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