more on Simplifier rules, based on old material;

refurbished Simplifier examples;

more on the Simplifier, based on old material;

more concise/precise documentation;

tuned text

replaced relation by function - simplifies development

made SMLNJ happier

import Sublist rather than PrefixOrder to avoid unnecessary class instantiation

prefer explicit Random.seed

dropped dead code

tuned import order

tuned layout

fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies

create temp directory if not already created

merged

new theory IMP/Finite_Reachable

avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit

centralized term printing code

thread context correctly when printing backquoted facts

dropped dead code; tuned theory text

modernized, simplified and compacted oracle and proof method glue code; corrected slips with poly.Pw and Orderings.less(_eq)

merged

fixed underscores

moved lemmas into projective_family; added header for theory Projective_Family

removed redundant/unnecessary assumptions from projective_family

assume probability spaces; allow empty index set

added projective_family; generalized generator in product_prob_space to projective_family

moved lemmas further up

tuned proofs

using hyp_subst_tac that allows to pass the current simpset to avoid the renamed bound variable warning in the simplifier