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

a few notations changed in HOL/BNF/Examples/Derivation_Trees

ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package

adding test cases for f x y : S patterns in set_comprehension_pointfree simproc

tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage

term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage

extending preprocessing of simproc to rewrite subset inequality into membership of powerset

update ROOT with teh directory change in BNF

changed name of BNF/Example directory from Infinite_Derivation_Trees to Derivation_Trees

retain info dockable state via educated guess on window focus;

support for more informative errors in lazy enumerations;