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
2011-07-18 bulwahn 2011-07-18 adding narrowing instances for real and rational
2011-07-18 bulwahn 2011-07-18 adapting quickcheck based on the analysis of the predicate compiler
2011-07-18 bulwahn 2011-07-18 adapting prolog-based tester
2011-07-18 bulwahn 2011-07-18 quickcheck does not deactivate testers if none are given
2011-07-18 bulwahn 2011-07-18 adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
2011-07-18 bulwahn 2011-07-18 renaming quickcheck_tester to quickcheck_batch_tester; tuned
2011-07-18 bulwahn 2011-07-18 changing parser in quickcheck to activate and deactivate the testers
2011-07-18 bulwahn 2011-07-18 adapting SML_Quickcheck to new quickcheck infrastructure
2011-07-18 bulwahn 2011-07-18 enabling parallel execution of testers but removing more informative quickcheck output
2011-07-18 bulwahn 2011-07-18 changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
2011-07-18 bulwahn 2011-07-18 removing generator registration
2011-07-18 bulwahn 2011-07-18 parametrized test_term functions in quickcheck
2011-07-18 bulwahn 2011-07-18 adding random, exhaustive and SML quickcheck as testers
2011-07-17 haftmann 2011-07-17 more on complement
2011-07-17 haftmann 2011-07-17 more on complement
2011-07-17 haftmann 2011-07-17 more consistent theorem names
2011-07-17 haftmann 2011-07-17 more lemmas about SUP
2011-07-17 haftmann 2011-07-17 structuring duals together
2011-07-17 haftmann 2011-07-17 merged
2011-07-17 haftmann 2011-07-17 more lemmas about Sup
2011-07-17 haftmann 2011-07-17 generalized INT_anti_mono
2011-07-17 haftmann 2011-07-17 moving UNIV = ... equations to their proper theories
2011-07-17 haftmann 2011-07-17 further generalization from sets to complete lattices
2011-07-17 blanchet 2011-07-17 fixed lambda-liftg: must ensure the formulas are in close form
2011-07-17 blanchet 2011-07-17 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)