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

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

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

merged

added constraint for Eq^- in Nitpick's implementation of the monotonicity calculus

change the order in which Nitpick tries SAT solvers;
so that the binary JNIs come further down the list and can
easily be overridden

Fixed splitting of div and mod on integers (split theorem differed from implementation).

merged

Fixed splitting of div and mod on integers (split theorem differed from implementation).

init_theory: Runtime.controlled_execution for proper exception trace etc.;

eliminated slightly odd name space grouping -- now managed by Isar toplevel;

implicit name space grouping for theory/local_theory transactions;

uniform new_group/reset_group;
tuned signature;