Tue, 24 Jun 2014 12:35:49 +0200 blanchet added another experimental engine
Tue, 24 Jun 2014 12:35:43 +0200 blanchet tweaked experimental setup
Tue, 24 Jun 2014 08:20:00 +0200 blanchet changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)
Tue, 24 Jun 2014 08:19:58 +0200 blanchet use strings to communicate with external process, to ease debugging
Tue, 24 Jun 2014 08:19:57 +0200 blanchet added 'dummy_thf_ml' prover for experiments with HOLyHammer
Tue, 24 Jun 2014 08:19:56 +0200 blanchet phantoms may also occur in THF1
Tue, 24 Jun 2014 08:19:55 +0200 blanchet added experimental MaSh engine
Tue, 24 Jun 2014 08:19:55 +0200 blanchet move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
Tue, 24 Jun 2014 08:19:54 +0200 blanchet help reconstruction of Z3 skolemization by weakening formulas a bit
Tue, 24 Jun 2014 08:19:22 +0200 blanchet supports gradual skolemization (cf. Z3) by threading context through correctly
Tue, 24 Jun 2014 08:19:22 +0200 blanchet given two one-liners, only show the best of the two
Tue, 24 Jun 2014 08:19:22 +0200 blanchet don't generate Isar proof skeleton for what amounts to a one-line proof
Tue, 24 Jun 2014 08:19:22 +0200 blanchet don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)
Sun, 22 Jun 2014 12:37:55 +0200 nipkow r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
Sat, 21 Jun 2014 15:46:52 +0200 nipkow added [simp]
Sat, 21 Jun 2014 10:41:02 +0200 ballarin Two basic lemmas on bij_betw.
Fri, 20 Jun 2014 09:55:31 +0200 blanchet changed default MaSh parameters based on (in vitro) evaluation
Fri, 20 Jun 2014 09:42:36 +0200 blanchet made 'tptp_graph' more liberal (why reject TFF?)
Wed, 18 Jun 2014 17:42:24 +0200 blanchet made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
Wed, 18 Jun 2014 17:42:24 +0200 blanchet more MaSh engine variations, for evaluations
Wed, 18 Jun 2014 17:42:24 +0200 blanchet split parameter into two
Wed, 18 Jun 2014 14:31:32 +0200 hoelzl filters are easier to define with INF on filters.
Wed, 18 Jun 2014 07:31:12 +0200 hoelzl moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
Wed, 18 Jun 2014 15:23:40 +0200 blanchet more generous formula -- there are lots of duplicates out there
Wed, 18 Jun 2014 14:19:42 +0200 blanchet automatically learn MaSh facts also in 'blocking' mode
Wed, 18 Jun 2014 13:23:09 +0200 blanchet enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
Tue, 17 Jun 2014 18:41:44 +0200 ballarin Lemmas contributed by Joachim Breitner.
Tue, 17 Jun 2014 18:33:34 +0200 blanchet reintroduce atomize in Waldmeister code
Tue, 17 Jun 2014 16:02:49 +0200 blanchet changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
Mon, 16 Jun 2014 19:44:02 +0200 blanchet compile
Mon, 16 Jun 2014 19:42:44 +0200 blanchet integrated new Waldmeister code with 'sledgehammer' command
Mon, 16 Jun 2014 19:41:42 +0200 blanchet fixed parsing of one-argument 'file()' in TSTP files
Mon, 16 Jun 2014 19:41:01 +0200 blanchet use right delimiters for Waldmeister proofs
Mon, 16 Jun 2014 19:41:00 +0200 blanchet added 'waldmeister_new' as ATP
Mon, 16 Jun 2014 19:40:59 +0200 blanchet simplified code
Mon, 16 Jun 2014 19:40:04 +0200 blanchet moved code around
Mon, 16 Jun 2014 19:39:41 +0200 blanchet give Z3 TPTP proofs a chance
Mon, 16 Jun 2014 19:18:10 +0200 blanchet fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
Mon, 16 Jun 2014 17:52:33 +0200 hoelzl add more derivative and continuity rules for complex-values functions
Mon, 16 Jun 2014 16:21:52 +0200 fleury Moving the remote prefix deleting on Sledgehammer's side
Mon, 16 Jun 2014 16:21:39 +0200 fleury Correcting the type parser
Mon, 16 Jun 2014 16:18:34 +0200 fleury imported patch leo2_skolem_simplication
Mon, 16 Jun 2014 16:18:15 +0200 fleury add support for Isar reconstruction for thf1 ATP provers like Leo-II.
Mon, 16 Jun 2014 13:19:48 +0200 hoelzl lemmas about the moments of the normal distribution
Fri, 13 Jun 2014 14:49:59 +0100 paulson NEWS
Fri, 13 Jun 2014 14:08:20 +0200 hoelzl properties of normal distributed random variables (by Sudeep Kanav)
Fri, 13 Jun 2014 07:05:01 +0200 nipkow announce Tree
Thu, 12 Jun 2014 21:23:28 +0200 nipkow new theory of binary trees
Thu, 12 Jun 2014 18:02:39 +0200 haftmann formal variable name: IVar NONE is strictly spoken not supported on lhs of function definitions, e.g. in Scala
Thu, 12 Jun 2014 18:47:27 +0200 nipkow merged
Thu, 12 Jun 2014 18:47:16 +0200 nipkow added [simp]
Thu, 12 Jun 2014 17:50:49 +0200 blanchet tuning
Thu, 12 Jun 2014 17:10:12 +0200 blanchet renamed Sledgehammer options
Thu, 12 Jun 2014 17:02:03 +0200 blanchet removed dead code
Thu, 12 Jun 2014 17:02:03 +0200 blanchet reintroduced vital 'Thm.transfer'
Thu, 12 Jun 2014 17:02:03 +0200 blanchet tuned dependencies
Thu, 12 Jun 2014 17:02:03 +0200 blanchet updated docs
Thu, 12 Jun 2014 17:02:03 +0200 blanchet added support for CVC4 in SMT2
Thu, 12 Jun 2014 17:02:03 +0200 blanchet don't ask proof-disabled solvers to do proofs
Thu, 12 Jun 2014 17:02:03 +0200 blanchet tuning
Thu, 12 Jun 2014 17:02:03 +0200 blanchet took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
Thu, 12 Jun 2014 17:02:02 +0200 blanchet made CVC3 work with SMT2 stack
Thu, 12 Jun 2014 15:47:36 +0200 hoelzl properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
Wed, 11 Jun 2014 13:39:38 +0200 hoelzl clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
Thu, 12 Jun 2014 08:48:59 +0200 haftmann uniform treatment of trivial unit instances: simplify by default, unfold in code preprocessor
Thu, 12 Jun 2014 01:00:49 +0200 blanchet adapted examples to changes in SMT triggers
Thu, 12 Jun 2014 01:00:49 +0200 blanchet reduces Sledgehammer dependencies
Thu, 12 Jun 2014 01:00:49 +0200 blanchet eliminate dependency of SMT2 module on 'list'
Thu, 12 Jun 2014 01:00:49 +0200 blanchet tuning
Thu, 12 Jun 2014 01:00:49 +0200 blanchet removed subsumed record-related code, now that records are registered as 'ctr_sugar'
Thu, 12 Jun 2014 01:00:49 +0200 blanchet made lookup more robust in the face of missing (dummy) case constant
Thu, 12 Jun 2014 01:00:49 +0200 blanchet use 'ctr_sugar' abstraction in SMT(2)
Thu, 12 Jun 2014 01:00:49 +0200 blanchet register record extensions as freely generated types
Wed, 11 Jun 2014 18:22:05 +0200 haftmann mixin definitions are within scope of "for"s of import expression
Wed, 11 Jun 2014 18:22:04 +0200 haftmann proper proof context transfer wrt. background theory avoids ad-hoc restore operation
Wed, 11 Jun 2014 19:32:39 +0200 blanchet refactoring
Wed, 11 Jun 2014 19:32:12 +0200 blanchet moved generic code further up
Wed, 11 Jun 2014 19:15:55 +0200 blanchet tuned code
Wed, 11 Jun 2014 19:15:54 +0200 blanchet factor out SMT-LIB 2 type/term parsing from Z3-specific code
Wed, 11 Jun 2014 19:08:32 +0200 blanchet simplify slightly ATP proof generated for Z3
Wed, 11 Jun 2014 16:02:10 +0200 steckerm tuned whitespaces
Wed, 11 Jun 2014 15:44:09 +0200 blanchet updated contributors to include students
Wed, 11 Jun 2014 15:29:23 +0200 blanchet moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
Wed, 11 Jun 2014 11:28:46 +0200 blanchet adapted SMT examples to new, corrected handling of 'typedef'
Wed, 11 Jun 2014 11:28:46 +0200 blanchet fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
Wed, 11 Jun 2014 11:28:46 +0200 blanchet updated NEWS slightly
Wed, 11 Jun 2014 11:28:46 +0200 blanchet updated docs w.r.t. Z3
Wed, 11 Jun 2014 11:28:46 +0200 blanchet rationalized CVC3 and Yices environment variable -- no need (unlike for Z3) to distinguish between old and new versions
Wed, 11 Jun 2014 11:28:46 +0200 blanchet removed '_new' sufffix in SMT2 solver names (in some cases)
Wed, 11 Jun 2014 11:28:46 +0200 blanchet removed old SMT module from Sledgehammer
Wed, 11 Jun 2014 08:58:42 +0200 blanchet got rid of 'listF' example, which is now subsumed by the real 'list' type
Tue, 10 Jun 2014 21:15:57 +0200 blanchet changed syntax of map: and rel: arguments to BNF-based datatypes
Tue, 10 Jun 2014 19:51:00 +0200 blanchet tuning
Tue, 10 Jun 2014 19:15:15 +0200 blanchet updated Z3 certificates
Tue, 10 Jun 2014 19:15:14 +0200 blanchet generate ':named' attributes in SMT-LIB 2 problems, to facilitate reconstruction
Tue, 10 Jun 2014 19:15:14 +0200 blanchet tuning
Tue, 10 Jun 2014 18:24:53 +0200 Andreas Lochbihler add type class instances for unit
Tue, 10 Jun 2014 12:16:22 +0200 blanchet use 'where' clause for selector default value syntax
Tue, 10 Jun 2014 11:38:53 +0200 blanchet tuning
Mon, 09 Jun 2014 16:08:30 +0200 nipkow added List.union
Mon, 09 Jun 2014 12:36:22 +0200 nipkow Sup/Inf on functions decoupled from complete_lattice.
Sun, 08 Jun 2014 23:30:53 +0200 haftmann tuned data structure
Sun, 08 Jun 2014 23:30:52 +0200 haftmann recovered level-free fishing for locale, accidentally lost in dce365931721
Sun, 08 Jun 2014 23:30:52 +0200 haftmann tuned terminology: emphasize stack-like nature of nested local theories
Sun, 08 Jun 2014 23:30:51 +0200 haftmann self-contained locale_declaration operation
Sun, 08 Jun 2014 23:30:51 +0200 haftmann 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
Sun, 08 Jun 2014 23:30:50 +0200 haftmann tuned
Sun, 08 Jun 2014 23:30:49 +0200 haftmann recovered structure of module, which got somehow convoluted due to incremental modifications
Sun, 08 Jun 2014 23:30:49 +0200 haftmann 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
Sun, 08 Jun 2014 23:30:48 +0200 haftmann revert effect of 63c7b29d29ac -- existing pervasive interpretation of class order for dvd etc. is too obstrusive at the moment
Sun, 08 Jun 2014 23:30:47 +0200 haftmann less ad-hoc verision of educated guess: guess identity of declaration morphism wrt. canonical morphism rather than observing particular effects of declaration morphisms only;
Sat, 07 Jun 2014 21:49:17 +0200 haftmann treat non-canonical interpretations of classes the same way as ordinary locale interpretations
Sat, 07 Jun 2014 08:16:03 +0200 haftmann tuned
Sat, 07 Jun 2014 08:16:03 +0200 haftmann avoid odd Named_Target.reinit altogether
Sat, 07 Jun 2014 08:16:03 +0200 haftmann clarified terminology: toplevel is interwined with named targets in particular, not with local theories in general
Sat, 07 Jun 2014 08:16:03 +0200 haftmann less baroque interface
Fri, 06 Jun 2014 19:19:46 +0200 haftmann dropped obscure and unused ad-hoc before_exit hook for named targets
Fri, 06 Jun 2014 12:36:06 +0200 nipkow added lemma
Thu, 05 Jun 2014 14:37:44 +0200 noschinl mira: USER_HOME must exist for building JEdit documentation
Fri, 06 Jun 2014 10:53:33 +0200 nipkow added lemmas
(0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 tip