2011-07-23 wenzelm 2011-07-23 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-07-23 wenzelm 2011-07-23 tuned;
2011-07-22 haftmann 2011-07-22 merged
2011-07-22 haftmann 2011-07-22 dropped errorneous hint
2011-07-21 haftmann 2011-07-21 moved some lemmas
2011-07-21 haftmann 2011-07-21 merged
2011-07-21 haftmann 2011-07-21 ereal is a complete_linorder instance
2011-07-20 haftmann 2011-07-20 class complete_linorder
2011-07-21 blanchet 2011-07-21 make "concealed" lambda translation sound
2011-07-21 bulwahn 2011-07-21 deactivating all quickcheck invocations until parallel invocation works safely
2011-07-21 bulwahn 2011-07-21 adapting two examples in Predicate_Compile_Examples
2011-07-20 blanchet 2011-07-20 use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
2011-07-20 Cezary Kaliszyk 2011-07-20 merge
2011-07-20 Cezary Kaliszyk 2011-07-20 Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal
2011-07-20 hoelzl 2011-07-20 add code generator setup and tests for ereal
2011-07-20 boehmes 2011-07-20 removed debugging facilities accidentally left in the committed code
2011-07-20 boehmes 2011-07-20 more precise dependencies
2011-07-20 boehmes 2011-07-20 merged
2011-07-20 boehmes 2011-07-20 generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
2011-07-20 boehmes 2011-07-20 moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)
2011-07-20 boehmes 2011-07-20 removed old (unused) SMT monomorphizer
2011-07-20 krauss 2011-07-20 added UNION
2011-07-20 hoelzl 2011-07-20 merged
2011-07-19 hoelzl 2011-07-19 rename Fin to enat
2011-07-19 hoelzl 2011-07-19 add ereal to typeclass infinity
2011-07-19 hoelzl 2011-07-19 add nat => enat coercion
2011-07-19 hoelzl 2011-07-19 Introduce infinity type class
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-07-19 hoelzl 2011-07-19 rename Nat_Infinity (inat) to Extended_Nat (enat)
2011-07-20 Cezary Kaliszyk 2011-07-20 HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
2011-07-20 kleing 2011-07-20 build an image for HOL-IMP
2011-07-20 bulwahn 2011-07-20 deactivating quickcheck invocation in this example until the Interrupt issue is understood
2011-07-20 bulwahn 2011-07-20 removing inner time limits in quickcheck
2011-07-20 bulwahn 2011-07-20 updating documentation about quickcheck; adding information about try
2011-07-20 bulwahn 2011-07-20 adapting example in Predicate_Compile_Examples
2011-07-20 bulwahn 2011-07-20 exporting function in quickcheck; adapting mutabelle script
2011-07-20 bulwahn 2011-07-20 more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
2011-07-20 bulwahn 2011-07-20 making messages more informative
2011-07-20 bulwahn 2011-07-20 only use exhaustive testing in this quickcheck example
2011-07-20 blanchet 2011-07-20 parse equalities correctly in Nitrox parser
2011-07-20 blanchet 2011-07-20 pass type arguments to lambda-lifted Frees, to account for polymorphism
2011-07-20 blanchet 2011-07-20 generate slightly less type information -- this should be sound since type arguments should keep things cleanly apart
2011-07-20 blanchet 2011-07-20 avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
2011-07-20 blanchet 2011-07-20 remove offset from Mirabelle output
2011-07-19 krauss 2011-07-19 the HOL4PROOFS setting is actually HOL4_PROOFS
2011-07-19 haftmann 2011-07-19 merged
2011-07-18 haftmann 2011-07-18 proof tuning
2011-07-18 haftmann 2011-07-18 generalization; various notation and proof tuning
2011-07-18 haftmann 2011-07-18 avoid misunderstandable names
2011-07-18 haftmann 2011-07-18 moved lemmas to appropriate theory
2011-07-19 krauss 2011-07-19 forgotten qualifier
2011-07-19 krauss 2011-07-19 values_timeout defaults to 600.0 on SML/NJ -- saves us from cluttering all theories equivalent declarations
2011-07-18 krauss 2011-07-18 killed use of PolyML.makestring
2011-07-18 krauss 2011-07-18 added experimental mira configuration for HOL Light importer
2011-07-18 boehmes 2011-07-18 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
2011-07-18 bulwahn 2011-07-18 unactivating narrowing-based quickcheck by default
2011-07-18 bulwahn 2011-07-18 making active configuration public in narrowing-based quickcheck
2011-07-18 bulwahn 2011-07-18 declare tester in this quickcheck example
2011-07-18 bulwahn 2011-07-18 adding code equations for partial_term_of for rational numbers
2011-07-18 bulwahn 2011-07-18 adapting an experimental setup to changes in quickcheck's infrastructure