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

avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;
2010-05-29, by wenzelm
define_state/new_state: provide state immediately, which is now lazy;
2010-05-29, by wenzelm
force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
2010-05-29, by wenzelm
future result: retain plain Interrupt for vacuous group exceptions;
2010-05-29, by wenzelm
remove two examples, now that the definition of "fst" and "snd" has changed
2010-05-28, by blanchet
merged
2010-05-28, by wenzelm
Got rid of a warning about duplicate rewrite rules.
2010-05-28, by webertj
accumulate only local results -- no proper history support yet;
2010-05-28, by wenzelm
avoid deprecated Iterator.fromArray;
2010-05-28, by wenzelm
more compiler warnings;
2010-05-28, by wenzelm
eliminated hard tabs;
2010-05-28, by wenzelm
assume given SCALA_HOME, e.g. from component settings or external setup;
2010-05-28, by wenzelm
merged
2010-05-28, by wenzelm
merged
2010-05-28, by blanchet
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
2010-05-28, by blanchet
Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes
2010-05-27, by blanchet
make Nitpick "show_all" option behave less surprisingly
2010-05-27, by blanchet
merged
2010-05-28, by haftmann
avoid reference to thm PairE
2010-05-28, by haftmann
more coherent theory structure; tuned headings
2010-05-28, by haftmann
made SML/NJ quite happy;
2010-05-28, by wenzelm
reuse main view.font from jEdit;
2010-05-28, by wenzelm
deleted some old fonts;
2010-05-28, by wenzelm
also set font for printing, which actually works out of the box;
2010-05-28, by wenzelm
lib/Tools/makeall does not hardiwre logics;
2010-05-28, by wenzelm
discontinued Sun/Solaris tests;
2010-05-28, by wenzelm
some updates for release;
2010-05-28, by wenzelm
merged
2010-05-27, by wenzelm
added function update examples and set examples
2010-05-27, by boehmes
updated SMT certificates
2010-05-27, by boehmes
sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
2010-05-27, by boehmes
merged
2010-05-27, by boehmes
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
2010-05-27, by boehmes
made script executable
2010-05-27, by boehmes
use Z3's builtin support for div and mod
2010-05-27, by boehmes
moved SMT into the HOL image
2010-05-27, by boehmes
slightly odd workaround to ignore markup that is typically displaced;
2010-05-27, by wenzelm
substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up;
2010-05-27, by wenzelm
further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;
2010-05-27, by wenzelm
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27, by wenzelm
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-27, by wenzelm
misc updates for release;
2010-05-27, by wenzelm
constant Rat.normalize needs to be qualified;
2010-05-27, by wenzelm
merged
2010-05-27, by wenzelm
merged
2010-05-27, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
dropped legacy theorem bindings
2010-05-26, by haftmann
normalized references to constant "split"
2010-05-26, by haftmann
Revise locale test theory layout.
2010-05-26, by ballarin
Merge mixins of distinct interpretations with same base.
2010-05-26, by ballarin
indicate prospective properties;
2010-05-27, by wenzelm
clarified auto_update vs. update;
2010-05-27, by wenzelm
more reactive message handling, notably for follow_caret mode;
2010-05-27, by wenzelm
Command.toString: include id for debugging;
2010-05-27, by wenzelm
merged
2010-05-26, by wenzelm
refer to polyml-5.3.0-old for ppc-darwin;
2010-05-26, by wenzelm
try logical and theory abstraction before full abstraction (avoids warnings of linarith)
2010-05-26, by boehmes

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

isabelle