2010-10-05 krauss use Cache structure instead of passing tables around explicitly
2010-10-05 haftmann merged
2010-10-05 haftmann lemmas fold_commute and fold_commute_apply
2010-05-07 krauss spelling
2010-10-04 haftmann adjusted to inductive characterization of sorted
2010-10-04 haftmann tuned whitespace
2010-10-04 haftmann turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
2010-10-04 haftmann turned distinct and sorted into inductive predicates: yields nice induction principles for free
2010-10-04 haftmann turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
2010-10-02 blanchet some Poly/ML-specific debugging code escaped in the wild -- comment it out
2010-10-01 haftmann merged
2010-10-01 haftmann avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
2010-10-01 haftmann moved ML_Context.value to Code_Runtime
2010-10-01 haftmann constant `contents` renamed to `the_elem`
2010-10-01 blanchet merged
2010-10-01 blanchet tune whitespace
2010-10-01 blanchet rename bound variables after skolemizing, if the axiom of choice is available
2010-10-01 blanchet tuning
2010-10-01 blanchet rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
2010-10-01 blanchet tune bound names
2010-10-01 blanchet merged
2010-10-01 blanchet avoid dependency on "int"
2010-10-01 blanchet make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
2010-10-01 blanchet added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
2010-10-01 blanchet compute quantifier dependency graph in new skolemizer
2010-10-01 blanchet tuning
2010-10-01 blanchet compute substitutions in new skolemizer
2010-09-30 blanchet encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip