2014-06-12 blanchet 2014-06-12 reduces Sledgehammer dependencies
2014-06-12 blanchet 2014-06-12 eliminate dependency of SMT2 module on 'list'
2014-06-12 blanchet 2014-06-12 tuning
2014-06-12 blanchet 2014-06-12 removed subsumed record-related code, now that records are registered as 'ctr_sugar'
2014-06-12 blanchet 2014-06-12 made lookup more robust in the face of missing (dummy) case constant
2014-06-12 blanchet 2014-06-12 use 'ctr_sugar' abstraction in SMT(2)
2014-06-12 blanchet 2014-06-12 register record extensions as freely generated types
2014-06-11 haftmann 2014-06-11 mixin definitions are within scope of "for"s of import expression
2014-06-11 haftmann 2014-06-11 proper proof context transfer wrt. background theory avoids ad-hoc restore operation
2014-06-11 blanchet 2014-06-11 refactoring
2014-06-11 blanchet 2014-06-11 moved generic code further up
2014-06-11 blanchet 2014-06-11 tuned code
2014-06-11 blanchet 2014-06-11 factor out SMT-LIB 2 type/term parsing from Z3-specific code
2014-06-11 blanchet 2014-06-11 simplify slightly ATP proof generated for Z3
2014-06-11 steckerm 2014-06-11 tuned whitespaces
2014-06-11 blanchet 2014-06-11 updated contributors to include students
2014-06-11 blanchet 2014-06-11 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
2014-06-11 blanchet 2014-06-11 adapted SMT examples to new, corrected handling of 'typedef'
2014-06-11 blanchet 2014-06-11 fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
2014-06-11 blanchet 2014-06-11 updated NEWS slightly
2014-06-11 blanchet 2014-06-11 updated docs w.r.t. Z3
2014-06-11 blanchet 2014-06-11 rationalized CVC3 and Yices environment variable -- no need (unlike for Z3) to distinguish between old and new versions
2014-06-11 blanchet 2014-06-11 removed '_new' sufffix in SMT2 solver names (in some cases)
2014-06-11 blanchet 2014-06-11 removed old SMT module from Sledgehammer
2014-06-11 blanchet 2014-06-11 got rid of 'listF' example, which is now subsumed by the real 'list' type
2014-06-10 blanchet 2014-06-10 changed syntax of map: and rel: arguments to BNF-based datatypes
2014-06-10 blanchet 2014-06-10 tuning
2014-06-10 blanchet 2014-06-10 updated Z3 certificates
2014-06-10 blanchet 2014-06-10 generate ':named' attributes in SMT-LIB 2 problems, to facilitate reconstruction
2014-06-10 blanchet 2014-06-10 tuning
2014-06-10 Andreas Lochbihler 2014-06-10 add type class instances for unit
2014-06-10 blanchet 2014-06-10 use 'where' clause for selector default value syntax
2014-06-10 blanchet 2014-06-10 tuning
2014-06-09 nipkow 2014-06-09 added List.union
2014-06-09 nipkow 2014-06-09 Sup/Inf on functions decoupled from complete_lattice.
2014-06-08 haftmann 2014-06-08 tuned data structure
2014-06-08 haftmann 2014-06-08 recovered level-free fishing for locale, accidentally lost in dce365931721
2014-06-08 haftmann 2014-06-08 tuned terminology: emphasize stack-like nature of nested local theories
2014-06-08 haftmann 2014-06-08 self-contained locale_declaration operation
2014-06-08 haftmann 2014-06-08 yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
2014-06-08 haftmann 2014-06-08 tuned
2014-06-08 haftmann 2014-06-08 recovered structure of module, which got somehow convoluted due to incremental modifications
2014-06-08 haftmann 2014-06-08 re-unified approach towards class and locale consts, with refined terminology: foo_const_declaration denotes declaration for a particular logical layer, foo_const the full stack for a particular target
2014-06-08 haftmann 2014-06-08 revert effect of 63c7b29d29ac -- existing pervasive interpretation of class order for dvd etc. is too obstrusive at the moment
2014-06-08 haftmann 2014-06-08 less ad-hoc verision of educated guess: guess identity of declaration morphism wrt. canonical morphism rather than observing particular effects of declaration morphisms only; n.b. this fullfills promise given in 63c7b29d29ac
2014-06-07 haftmann 2014-06-07 treat non-canonical interpretations of classes the same way as ordinary locale interpretations
2014-06-07 haftmann 2014-06-07 tuned
2014-06-07 haftmann 2014-06-07 avoid odd Named_Target.reinit altogether
2014-06-07 haftmann 2014-06-07 clarified terminology: toplevel is interwined with named targets in particular, not with local theories in general
2014-06-07 haftmann 2014-06-07 less baroque interface
2014-06-06 haftmann 2014-06-06 dropped obscure and unused ad-hoc before_exit hook for named targets
2014-06-06 nipkow 2014-06-06 added lemma
2014-06-05 noschinl 2014-06-05 mira: USER_HOME must exist for building JEdit documentation
2014-06-06 nipkow 2014-06-06 added lemmas
2014-06-05 haftmann 2014-06-05 sharpened criterion: bare named target is only at the bottom level
2014-06-05 haftmann 2014-06-05 tuned
2014-06-05 traytel 2014-06-05 extended stream library
2014-06-05 haftmann 2014-06-05 be more explicit: made sml/nj happy
2014-06-05 haftmann 2014-06-05 always refine interpretation morphism using canonical constant's definition theorem
2014-06-04 noschinl 2014-06-04 set USER_HOME to affect also ISABELLE_PATH et al