2010-12-21 haftmann 2010-12-21 evaluator separating static and dynamic operations
2010-12-21 haftmann 2010-12-21 program is separate argument to serializer
2010-12-21 haftmann 2010-12-21 more explicit structure for serializer invocation
2010-12-21 nipkow 2010-12-21 merged
2010-12-21 nipkow 2010-12-21 tuned proof
2010-12-21 haftmann 2010-12-21 HOLogic.mk_id
2010-12-21 blanchet 2010-12-21 avoid weird symbols in path
2010-12-21 blanchet 2010-12-21 mechanism to keep SMT input and output files around in Mirabelle
2010-12-21 blanchet 2010-12-21 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; removed "is_builtin_ext", which is too limited an API to be useful in light of the aforementioned restriction
2010-12-21 blanchet 2010-12-21 added "smt_triggers" option to experiment with triggers in Sledgehammer; renamings (for consistency)
2010-12-21 blanchet 2010-12-21 enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day
2010-12-20 wenzelm 2010-12-20 Cygwin: Poly/ML 5.4.0 requires libgmp3;
2010-12-20 wenzelm 2010-12-20 updated to polyml-5.4.0;
2010-12-20 wenzelm 2010-12-20 tuned;
2010-12-20 wenzelm 2010-12-20 updated for Poly/ML 5.4.0;
2010-12-20 boehmes 2010-12-20 merged
2010-12-20 boehmes 2010-12-20 avoid ML structure aliases (especially single-letter abbreviations)
2010-12-20 boehmes 2010-12-20 added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions
2010-12-20 huffman 2010-12-20 merged
2010-12-20 huffman 2010-12-20 configure domain package to work with HOL option type
2010-12-20 huffman 2010-12-20 make internal proofs for deflation and isodefl theorems more robust, by avoiding calls to the simplifier for beta-reduction
2010-12-20 huffman 2010-12-20 simplify proofs
2010-12-20 huffman 2010-12-20 beta-reduction simproc uses lemma Abs_cfun_inverse2 instead of beta_cfun, to be more robust against eta-contraction
2010-12-20 huffman 2010-12-20 configure domain package to work with HOL sum type
2010-12-20 huffman 2010-12-20 replace list_map function with an abbreviation
2010-12-20 blanchet 2010-12-20 merged
2010-12-20 blanchet 2010-12-20 run SPASS and Vampire in SOS mode only if >= 50 facts are passed -- otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy
2010-12-20 blanchet 2010-12-20 disable feature that was enabled by mistake
2010-12-20 blanchet 2010-12-20 make exceptions more transparent in "debug" mode
2010-12-20 blanchet 2010-12-20 remove spurious line
2010-12-20 blanchet 2010-12-20 use the options provided by Stephan Schulz -- much better
2010-12-20 blanchet 2010-12-20 optionally supply constant weights to E -- turned off by default until properly parameterized
2010-12-20 haftmann 2010-12-20 merged
2010-12-20 haftmann 2010-12-20 type_lifting for predicates
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
2010-12-20 wenzelm 2010-12-20 some attempts to fit diagnostic output into regular TTY (75-80 characters per line);
2010-12-20 wenzelm 2010-12-20 tuned/clarified some component settings; explicit comments about common mistakes;
2010-12-20 wenzelm 2010-12-20 slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version); more robust rm_tree -- somewhat dangerous and not exported; tuned;
2010-12-20 wenzelm 2010-12-20 purged some comments (Locale_Test is already clean thanks to configuration options);
2010-12-20 wenzelm 2010-12-20 actually enable show_hyps option, unlike local_setup in 6da953d30f48 which merely affects the (temporary) auxiliary context;
2010-12-20 boehmes 2010-12-20 merged
2010-12-20 boehmes 2010-12-20 updated SMT certificates
2010-12-20 boehmes 2010-12-20 re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
2010-12-20 boehmes 2010-12-20 derived SMT solver classes override inherited properties (properties of derived classes have a higher priority than properties of base classes)
2010-12-20 boehmes 2010-12-20 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
2010-12-20 haftmann 2010-12-20 merge
2010-12-17 haftmann 2010-12-17 more convenient order of type variables
2010-12-19 huffman 2010-12-19 rename function cprod_map to prod_map
2010-12-19 huffman 2010-12-19 switch to transparent ascription, to avoid warning messages
2010-12-19 huffman 2010-12-19 types -> type_synonym
2010-12-19 huffman 2010-12-19 fix typo
2010-12-19 huffman 2010-12-19 merged
2010-12-19 huffman 2010-12-19 use deflations over type 'udom u' to represent predomains; removed now-unnecessary class liftdomain;
2010-12-19 huffman 2010-12-19 add lemma u_map_oo
2010-12-19 huffman 2010-12-19 replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
2010-12-19 huffman 2010-12-19 minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
2010-12-19 huffman 2010-12-19 powerdomain theories require class 'bifinite' instead of 'domain'
2010-12-19 huffman 2010-12-19 type 'defl' takes a type parameter again (cf. b525988432e9)
2010-12-19 huffman 2010-12-19 reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
2010-12-19 huffman 2010-12-19 renamed Bifinite.thy to Representable.thy