Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-64
+64
+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 JavaScript-enabled browsers.
news
2013-12-05, by Andreas Lochbihler
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
2013-12-05, by Andreas Lochbihler
merge
2013-12-03, by panny
generate "code" theorems for incomplete definitions
2013-12-02, by panny
updated keywords
2013-12-02, by blanchet
added 'no_code' option
2013-12-02, by blanchet
killed obsolete artifact
2013-12-02, by blanchet
revert making 'map_cong' a 'cong' -- it breaks too many proofs in the AFP
2013-12-02, by blanchet
avoid user-level 'Specification.definition' for low-level definitions
2013-12-02, by blanchet
repaired inconsistency introduced in transiting to 'Local_Theory.define'
2013-12-02, by blanchet
docs for forgotten BNF theorems
2013-12-02, by blanchet
tuning
2013-12-02, by blanchet
added 'cong' attribute to 'map_cong'
2013-12-02, by blanchet
avoid user-level 'Specification.definition' for internal constructions (to avoid e.g. automatic code generation behavior)
2013-12-02, by blanchet
don't try to register code equations in a locale with assumptions
2013-12-02, by blanchet
minor doc update
2013-12-02, by blanchet
generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)
2013-12-02, by blanchet
simpler code
2013-12-02, by blanchet
more work towards "exhaustive"
2013-12-01, by panny
Backed out changeset: a8ad7f6dd217---bypassing Main breaks theories that use \<inf> or \<sup>
2013-11-29, by traytel
set_comprehension_pointfree simproc causes to many surprises if enabled by default
2013-11-29, by traytel
tuned
2013-11-28, by nipkow
updated docs
2013-11-28, by blanchet
added Riss3g
2013-11-28, by blanchet
reduce dependency (toward move to 'HOL')
2013-11-28, by blanchet
cleaned up indirect dependency
2013-11-28, by blanchet
tuned
2013-11-28, by nipkow
prefer sort-stripping const_typ over Sign.the_const_type whenever appropriate
2013-11-28, by haftmann
prefer name-normalizing devarify over unvarifyT whenever appropriate
2013-11-28, by haftmann
some documentation
2013-11-27, by traytel
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
2013-11-27, by traytel
remove junk
2013-11-27, by Andreas Lochbihler
revert 4af7c82463d3 and document type class problem in Haskell
2013-11-27, by Andreas Lochbihler
merged
2013-11-27, by Andreas Lochbihler
no ord instance for String.literal in Haskell when list is also ordered lexicographically
2013-11-20, by Andreas Lochbihler
implement comparisons on String.literal by target-language comparisons
2013-11-20, by Andreas Lochbihler
instantiate linorder for String.literal by lexicographic order
2013-11-20, by Andreas Lochbihler
setup lifting/transfer for String.literal
2013-11-20, by Andreas Lochbihler
add predicate version of lexicographic order on lists
2013-11-20, by Andreas Lochbihler
merge
2013-11-26, by panny
prevent exception when equations for a function are missing;
2013-11-25, by panny
Add Zorn to HOL-Library
2013-11-26, by hoelzl
made SML/NJ happier
2013-11-26, by traytel
NEWS
2013-11-26, by traytel
even more precise NEWS
2013-11-25, by haftmann
mreged
2013-11-25, by paulson
Small simplifications to proofs
2013-11-25, by paulson
possibility to fold coercion inference error messages; tuned;
2013-11-25, by traytel
tweaks to the documentation
2013-11-25, by paulson
MaSH files should be ignored
2013-11-25, by paulson
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
2013-11-25, by traytel
adapt to 9733ab5c1df6
2013-11-25, by traytel
drop theorem duplicates
2013-11-25, by traytel
eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
2013-11-25, by traytel
typos
2013-11-25, by nipkow
tidied more proofs
2013-11-25, by paulson
cleaned up more messy proofs
2013-11-24, by paulson
merged
2013-11-24, by paulson
cleaned up some messy proofs
2013-11-24, by paulson
tuned
2013-11-24, by nipkow
replaced bad example
2013-11-24, by nipkow
polished some ancient proofs
2013-11-24, by paulson
merged
2013-11-23, by paulson
Simplified, tidied and generalised proofs esp of Binomial Theorem.
2013-11-23, by paulson
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-64
+64
+100
+300
+1000
+3000
+10000
tip