summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

finite precision computation to determine sign for comparison

positive precision for truncate; fixed precision for approximation of rationals; code for truncate

compute_real_of_float has not been used as code equation

tuned proof;

merged

slightly more robust re-initialization;

isabelle_scala_script is usually found by PATH;

within the Isabelle environment, main executables are always within PATH;

avoid global state change;

more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;