isabelle: Graph

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

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
added future;
2009-12-08, by wenzelm
depend on Java 1.6 after all;
2009-12-07, by wenzelm
basic support for IsabelleText fonts;
2009-12-07, by wenzelm
merged
2009-12-07, by haftmann
merged
2009-12-07, by haftmann
tuned inner structure
2009-12-07, by haftmann
merged Crude_Executable_Set into Executable_Set
2009-12-07, by haftmann
merged
2009-12-07, by blanchet
avoid using "prop_logic.ML" and "sat_solver.ML" twice (the other occurrence being in "FunDef.thy");
2009-12-07, by blanchet
better error message in Refute when specifying a non-existing SAT solver
2009-12-07, by blanchet
merged
2009-12-07, by wenzelm
updated certificate
2009-12-07, by boehmes
merged
2009-12-07, by haftmann
repaired read_const_expr, broken in 1e7ca47c6c3d
2009-12-07, by haftmann
merged
2009-12-07, by boehmes
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
2009-12-07, by boehmes
faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
2009-12-03, by boehmes

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle