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 JavaScript-enabled browsers.
merged
2009-12-14, by haftmann
improved crude deriving_show inference
2009-12-14, by haftmann
explicit name for function space
2009-12-14, by haftmann
make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits
2009-12-14, by blanchet
make Nitpick "Core" test more conservative, to avoid problems on Larry's machine
2009-12-14, by blanchet
made sml/nj happy
2009-12-14, by haftmann
also sort verification conditions before printing
2009-12-14, by boehmes
print assertions in a more natural order
2009-12-13, by boehmes
removed unique ids -- now in session.scala;
2009-12-11, by wenzelm
merged
2009-12-11, by wenzelm
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
2009-12-11, by wenzelm
Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;
2009-12-11, by wenzelm
merged
2009-12-11, by haftmann
repaired accident: do not forget module contents if there are no imports
2009-12-11, by haftmann
option width for Code_Target.code_of
2009-12-11, by haftmann
default_code_width is now proper theory data
2009-12-11, by haftmann
merged
2009-12-11, by boehmes
updated dependencies
2009-12-11, by boehmes
make assertion labels unique already when loading a verification condition,
2009-12-11, by boehmes
depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)
2009-12-11, by boehmes
merged
2009-12-11, by haftmann
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
2009-12-11, by haftmann
avoid dependency on implicit dest rule predicate1D in proofs
2009-12-11, by haftmann
merged
2009-12-11, by haftmann
NEWS
2009-12-11, by haftmann
merged
2009-12-11, by haftmann
merged
2009-12-09, by haftmann
take and drop as projections of chop
2009-12-09, by haftmann
explicit lower bound for index
2009-12-09, by haftmann
merged
2009-12-11, by paulson
merged
2009-12-10, by paulson
streamlined proofs
2009-12-10, by paulson
fixed typo
2009-12-10, by paulson
merged
2009-12-10, by wenzelm
only invoke metisFT if metis failed
2009-12-10, by boehmes
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
2009-12-10, by bulwahn
merged
2009-12-09, by haftmann
each import resides in its own line
2009-12-09, by haftmann
using existing lattice classes
2009-12-09, by haftmann
added get_data;
2009-12-10, by wenzelm
sealed XML.Tree;
2009-12-10, by wenzelm
simplified Cygwin setup, assuming 1.7 registry layout (version 1.5 suffers from upcaseenv problem anyway);
2009-12-09, by wenzelm
slightly more robust and less ambitious version of install_fonts;
2009-12-09, by wenzelm
more robust Cygwin.config: actually check Wow6432Node, prefer explicit CYGWIN_ROOT in any case;
2009-12-09, by wenzelm
merged
2009-12-09, by blanchet
merged
2009-12-09, by blanchet
merged
2009-12-08, by blanchet
made Nitpick work also for people who import "Plain" instead of "Main"
2009-12-08, by blanchet
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
2009-12-07, by blanchet
keep future Isabelle application entry point;
2009-12-09, by wenzelm
merged
2009-12-09, by wenzelm
also consider the fully-typed version of metis for Mirabelle measurements
2009-12-08, by boehmes
merged
2009-12-08, by boehmes
made SML/NJ happy
2009-12-08, by boehmes
simplified notion of empty module name
2009-12-08, by haftmann
commit
2009-12-08, by haftmann
resorted code equations from "old" number theory version
2009-12-08, by haftmann
merged
2009-12-08, by haftmann
split off evaluation mechanisms in separte module Code_Eval
2009-12-07, by haftmann
register_fonts: more precise error handling;
2009-12-08, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip