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
2010-12-17 huffman 2010-12-17 renamed CompactBasis.thy to Compact_Basis.thy
2010-12-19 boehmes 2010-12-19 merged
2010-12-19 boehmes 2010-12-19 updated SMT certificates
2010-12-19 boehmes 2010-12-19 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions); removed odd retyping during folify (instead, keep all terms well-typed)
2010-12-19 boehmes 2010-12-19 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general); hide internal constants z3div and z3mod; rewrite div/mod to z3div/z3mod instead of adding extra rules characterizing div/mod in terms of z3div/z3mod
2010-12-19 blanchet 2010-12-19 escape backticks in altstrings
2010-12-19 blanchet 2010-12-19 added a timestamp to Nitpick in verbose mode for debugging purposes; turn on verbose mode for the examples
2010-12-19 blanchet 2010-12-19 reduce the minimizer slack and add verbose information
2010-12-18 blanchet 2010-12-18 two layers of timeouts seem to be less reliable than a single layer
2010-12-18 blanchet 2010-12-18 move relevance filter into hard timeout
2010-12-18 blanchet 2010-12-18 handle timeouts in Mirabelle more gracefully
2010-12-18 blanchet 2010-12-18 made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever); disabled inductions (E and SPASS don't like them), but kept "ext" (seems more harmless)
2010-12-18 ballarin 2010-12-18 Add mixins to locale dependencies.
2010-12-18 ballarin 2010-12-18 Enable show_hyps, which appears to be set in batch mode but in an interactive session.
2010-12-18 ballarin 2010-12-18 Add mixins to sublocale command.
2010-12-18 blanchet 2010-12-18 tuning
2010-12-18 blanchet 2010-12-18 higher hard timeout
2010-12-18 blanchet 2010-12-18 lower threshold where the binary algorithm kick in and use the same value for automatic minimization
2010-12-18 blanchet 2010-12-18 compile
2010-12-18 blanchet 2010-12-18 let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
2010-12-18 blanchet 2010-12-18 use minimizing prover in Mirabelle
2010-12-18 blanchet 2010-12-18 renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
2010-12-18 blanchet 2010-12-18 factored out running a prover with (optionally) an implicit minimizer phrase
2010-12-17 wenzelm 2010-12-17 merged;
2010-12-17 blanchet 2010-12-17 remove option that doesn't work in Mirabelle anyway (Mirabelle uses Sledgehammer_Provers, not Sledgehammer_Run)
2010-12-17 blanchet 2010-12-17 more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
2010-12-17 blanchet 2010-12-17 convenient syntax for setting provers -- useful for debugging, not for general consumption and hence not documented
2010-12-17 blanchet 2010-12-17 merged
2010-12-17 blanchet 2010-12-17 put the SMT weights back where they belong, so that they're also used by Mirabelle
2010-12-17 blanchet 2010-12-17 added debugging option to find out how good the relevance filter was at identifying relevant facts
2010-12-17 wenzelm 2010-12-17 extra checking of name bindings for classes, types, consts; tuned;
2010-12-17 wenzelm 2010-12-17 more explicit references to structure Raw_Simplifier;
2010-12-17 wenzelm 2010-12-17 merged
2010-12-17 wenzelm 2010-12-17 merged
2010-12-17 wenzelm 2010-12-17 merged
2010-12-17 wenzelm 2010-12-17 Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
2010-12-17 haftmann 2010-12-17 dropped slightly odd Conv.tap_thy
2010-12-17 haftmann 2010-12-17 avoid slightly odd Conv.tap_thy
2010-12-17 haftmann 2010-12-17 allocate intermediate directories in module hierarchy
2010-12-17 blanchet 2010-12-17 export experimental options
2010-12-17 blanchet 2010-12-17 merged
2010-12-17 blanchet 2010-12-17 compile
2010-12-17 blanchet 2010-12-17 run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
2010-12-17 blanchet 2010-12-17 make timeout part of the SMT filter's tail
2010-12-17 blanchet 2010-12-17 merge
2010-12-17 blanchet 2010-12-17 split "smt_filter" into head and tail
2010-12-17 blanchet 2010-12-17 fewer facts to SInE-E
2010-12-17 blanchet 2010-12-17 Z3 sometimes reports two errors, with the first one referring to line 1 for some strange reason -- but it makes no sense to kill line 1, so we traverse the errors in reverse and consider only the last error