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
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.
more examples/tests
2014-09-08, by blanchet
tuned docs
2014-09-08, by blanchet
properly note theorems for split recursors
2014-09-08, by blanchet
tuning
2014-09-08, by blanchet
updated docs
2014-09-08, by blanchet
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
2014-09-08, by blanchet
tuning
2014-09-08, by blanchet
export one more ML function
2014-09-08, by blanchet
tuning
2014-09-08, by blanchet
more compatibility documentation
2014-09-08, by blanchet
refactored MaSh files to avoid regenerating exports on each eval
2014-09-08, by blanchet
added missing 'transpose'
2014-09-08, by blanchet
the kind is now always the empty string -- can no longer distinguish between user theorems and package theorems in a semi-reliable way
2014-09-08, by blanchet
made tactic more robust w.r.t. dead variables
2014-09-08, by traytel
restrictive options for class dependencies
2014-09-07, by haftmann
separated class_deps command into separate file
2014-09-07, by haftmann
Added translation for lambda expressions in terms.
2014-09-07, by steckerm
explicit theory with additional, less commonly used list operations
2014-09-07, by haftmann
generalized
2014-09-07, by haftmann
theory about sum and product on function bodies
2014-09-06, by haftmann
theory about lexicographic ordering on functions
2014-09-06, by haftmann
added various facts
2014-09-06, by haftmann
Generalised card_length_listsum to all m
2014-09-05, by paulson
added lemma
2014-09-05, by nipkow
updated docs
2014-09-05, by blanchet
pretend code generation is a ctr_sugar plugin
2014-09-05, by blanchet
updated docs
2014-09-05, by blanchet
added 'plugins' option to control which hooks are enabled
2014-09-05, by blanchet
introduced mechanism to filter interpretations
2014-09-05, by blanchet
fixed infinite loops in 'register' functions + more uniform API
2014-09-05, by blanchet
named interpretations
2014-09-05, by blanchet
centralized and cleaned up naming handling
2014-09-05, by blanchet
cleanup Wfrec; introduce dependent_wf/wellorder_choice
2014-09-04, by hoelzl
tuned Nitpick and Refute examples, which are too slow on some testing machines
2014-09-04, by blanchet
tweaked setup for datatype realizer
2014-09-04, by blanchet
renamed internal constant
2014-09-04, by blanchet
moved code around
2014-09-04, by blanchet
tuned size function generation
2014-09-04, by blanchet
tuning
2014-09-04, by blanchet
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
2014-09-03, by blanchet
tuned ctr_sugar database handling
2014-09-03, by blanchet
tuned BNF database handling
2014-09-03, by blanchet
intelligible errors instead of tactic failures
2014-09-03, by blanchet
reenabled yet another example
2014-09-03, by blanchet
made new tactic even more robust
2014-09-03, by blanchet
reenabled more examples
2014-09-03, by blanchet
fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
2014-09-03, by blanchet
reintroduced more examples
2014-09-03, by blanchet
improved tactic further
2014-09-03, by blanchet
reenabled example
2014-09-03, by blanchet
improved new countability tactic
2014-09-03, by blanchet
'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
2014-09-03, by blanchet
more robust exception handling
2014-09-03, by blanchet
added tests for new 'countable_datatype' proof method
2014-09-03, by blanchet
lessen the burden on the caller: sort where necessary in n2m
2014-09-03, by traytel
added compatibility function
2014-09-03, by blanchet
added countable tactic for new-style datatypes
2014-09-03, by blanchet
tuning
2014-09-03, by blanchet
registered 'typerep' as countable again
2014-09-03, by blanchet
moved old datatype material around
2014-09-03, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
tip