2014-09-01 blanchet 2014-09-01 ported Refute to use new datatypes when possible
2014-09-01 blanchet 2014-09-01 renamed BNF theories
2014-09-01 blanchet 2014-09-01 renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
2014-09-01 blanchet 2014-09-01 added primrec compatibility function
2014-09-01 blanchet 2014-09-01 more work on compatibility interfaces
2014-09-01 blanchet 2014-09-01 added compatibility examples/tests
2014-09-01 blanchet 2014-09-01 implemented compatibility definition of datatype
2014-09-01 blanchet 2014-09-01 implemented compatibility interpretation
2014-09-01 blanchet 2014-09-01 compile
2014-09-01 blanchet 2014-09-01 compile
2014-09-01 blanchet 2014-09-01 tuning
2014-09-01 blanchet 2014-09-01 compile
2014-09-01 blanchet 2014-09-01 more compatibility between old- and new-style datatypes
2014-09-01 blanchet 2014-09-01 added theory-based getters for convenience
2014-09-01 blanchet 2014-09-01 made transfer functions slightly more general
2014-09-01 blanchet 2014-09-01 tuned signatures
2014-09-01 blanchet 2014-09-01 tuning
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-09-01 blanchet 2014-09-01 tuned structure inclusion
2014-09-01 blanchet 2014-09-01 took out legacy material from 'HOL/Library/Library.thy'
2014-09-01 blanchet 2014-09-01 removed commented out parts
2014-09-01 blanchet 2014-09-01 tuned whitespace
2014-09-01 desharna 2014-09-01 document 'set_transfer'
2014-09-01 desharna 2014-09-01 generate 'set_transfer' for BNFs
2014-09-01 desharna 2014-09-01 document 'rel_transfer'
2014-09-01 desharna 2014-09-01 generate 'rel_transfer' for BNFs
2014-09-01 desharna 2014-09-01 document 'map_transfer'
2014-09-01 desharna 2014-09-01 note 'map_transfer' more often
2014-08-31 haftmann 2014-08-31 separated listsum material
2014-08-31 haftmann 2014-08-31 restored generic value slot, retaining default behaviour and separate approximate command
2014-08-31 haftmann 2014-08-31 convenient printing of (- 1 :: integer) after code evaluation
2014-08-30 haftmann 2014-08-30 inlined unused definition
2014-08-29 hoelzl 2014-08-29 add simp rules for divisions of numerals in floor and ceiling.
2014-08-29 desharna 2014-08-29 document 'disc_transfer'
2014-08-29 desharna 2014-08-29 generate 'disc_transfer' for (co)datatypes
2014-08-29 desharna 2014-08-29 document 'case_transfer'
2014-08-29 desharna 2014-08-29 generate 'case_transfer' for (co)datatypes
2014-08-28 blanchet 2014-08-28 renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
2014-08-28 blanchet 2014-08-28 reworked unskolemization for SPASS
2014-08-28 blanchet 2014-08-28 clarified docs
2014-08-28 blanchet 2014-08-28 gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
2014-08-28 blanchet 2014-08-28 prefer '0.2 ms' to '249 \<mu>s'
2014-08-28 blanchet 2014-08-28 use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
2014-08-28 blanchet 2014-08-28 fixed second computations
2014-08-28 blanchet 2014-08-28 merged minimize and auto_minimize
2014-08-28 blanchet 2014-08-28 pass options to remote Vampire
2014-08-28 blanchet 2014-08-28 removed show stuttering
2014-08-28 blanchet 2014-08-28 generate 'thesis' variable in Sledgehammer Isar proofs
2014-08-28 blanchet 2014-08-28 show microseconds as well (useful when playing with Isar proofs)
2014-08-28 blanchet 2014-08-28 tuned message
2014-08-28 blanchet 2014-08-28 made trace more informative when minimization is enabled
2014-08-28 blanchet 2014-08-28 took out one more occurrence of 'PolyML.makestring'
2014-08-28 blanchet 2014-08-28 try 'skolem' method first for Z3
2014-08-28 blanchet 2014-08-28 tuned tracing output (indirectly)
2014-08-28 blanchet 2014-08-28 going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
2014-08-28 blanchet 2014-08-28 moved skolem method
2014-08-28 blanchet 2014-08-28 added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
2014-08-28 blanchet 2014-08-28 tuned method description
2014-08-28 blanchet 2014-08-28 three-line 'obtain' format for generated Isar proofs
2014-08-28 wenzelm 2014-08-28 tuned;