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

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

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

- use TableFun instead of homebrew binary tree in am_interpreter.ML
- add Floats to HOL/Real

- introduce Pure/Tools directory
- add compute oracle to Pure/Tools

fold_map -> fold_yield, added transformator combinators, added selector combinator

changed orientation of bind_assoc rule

use qualified names for all constants

added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined

generalized types of monadic operators to class cpo; added match function for UU

added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.)
renamed simplification rules for abs (abs_of_pos, etc.)
renamed rules for multiplication and signs (mult_pos_pos, etc.)
moved lemmas involving fractions from NatSimprocs.thy
added setsum_mono3 to FiniteSet.thy
added simplification rules for powers to Parity.thy

experimental code to reduce the amount of type information in blast

tweaked