2009-11-17 ago blanchet comment out debugging code in Nitpick
2009-11-17 ago blanchet fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
2009-11-17 ago blanchet made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
2009-11-17 ago blanchet removed "debug := true" that shouldn't have been submitted in the first place
2009-11-17 ago hoelzl Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
2009-11-17 ago blanchet merged
2009-11-17 ago blanchet run Nitpick examples if Kodkodi is available
2009-11-17 ago wenzelm merged
2009-11-17 ago blanchet fixed "expect" of Nitpick examples to reflect latest changes in Nitpick
2009-11-17 ago blanchet merged
2009-11-17 ago blanchet use SAT solver that's available everywhere for this example
2009-11-17 ago blanchet invoke Kodkodi from Nitpick using new $KODKOD/bin/kodkodi script;
2009-11-17 ago blanchet merged
2009-11-16 ago blanchet added constraint for Eq^- in Nitpick's implementation of the monotonicity calculus
2009-11-16 ago blanchet change the order in which Nitpick tries SAT solvers;
2009-11-17 ago webertj Fixed splitting of div and mod on integers (split theorem differed from implementation).
2009-11-17 ago webertj merged
2009-11-17 ago webertj Fixed splitting of div and mod on integers (split theorem differed from implementation).
2009-11-17 ago wenzelm init_theory: Runtime.controlled_execution for proper exception trace etc.;
2009-11-17 ago wenzelm eliminated slightly odd name space grouping -- now managed by Isar toplevel;
2009-11-17 ago wenzelm implicit name space grouping for theory/local_theory transactions;
2009-11-17 ago wenzelm uniform new_group/reset_group;
2009-11-17 ago wenzelm eliminated dead code;
2009-11-16 ago wenzelm generalized procs for rewrite_proof: allow skeleton;
2009-11-16 ago wenzelm member/cons: slightly more correct treatment of multi-index, notably empty one;
2009-11-16 ago wenzelm merged
2009-11-16 ago webertj Fixed a typo in a comment.
2009-11-16 ago webertj Fixed a typo in a comment.
2009-11-16 ago paulson merged
2009-11-16 ago paulson A few more lemmas from Jeremy
2009-11-16 ago hoelzl removed hassize predicate
2009-11-16 ago hoelzl Added new lemmas to Euclidean Space by Robert Himmelmann
2009-11-16 ago wenzelm eliminated obsolete thm position stuff;
2009-11-16 ago wenzelm tuned signature;
2009-11-16 ago wenzelm guard future proofs by Goal.future_enabled;
2009-11-16 ago boehmes further explosion of HOL-Boogie verification conditions
2009-11-16 ago haftmann merged
2009-11-16 ago haftmann proper purge
2009-11-16 ago haftmann dropped obsolete documentation; updated generated sources
2009-11-16 ago blanchet merged
2009-11-13 ago blanchet removed a few global names in Nitpick (styp, nat_less, pairf)
2009-11-15 ago wenzelm add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature;
2009-11-15 ago wenzelm axiomatization: declare Spec_Rules, direct result;
2009-11-15 ago wenzelm use simultaneous Morphics.fact;
2009-11-15 ago wenzelm primitive defs: clarified def (axiom name) vs. description;
2009-11-15 ago wenzelm eliminated obsolete thm position tags;
2009-11-15 ago wenzelm permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);
2009-11-15 ago wenzelm provide actual Nitpick_HOL.extended_context;
2009-11-15 ago wenzelm tuned;
2009-11-15 ago wenzelm more accurate dependencies;
2009-11-15 ago wenzelm eliminated obsolete CVS Ids;
2009-11-15 ago schirmer merged
2009-11-15 ago schirmer added benchmark for large records
2009-11-14 ago schirmer merged
2009-11-14 ago schirmer clarified quick-and-dirty usage in record package;
2009-11-15 ago wenzelm simplified bulky metis proofs;
2009-11-15 ago wenzelm properly inlined @{lemma} antiqutations -- might also reduce proof terms a bit;
2009-11-14 ago wenzelm moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
2009-11-14 ago wenzelm include HOL-Boogie keywords by default;
2009-11-14 ago wenzelm eliminated obsolete CVS Ids;