| Wed, 11 Jun 2014 13:39:38 +0200 |
hoelzl |
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
|
changeset |
files
|
| Thu, 12 Jun 2014 08:48:59 +0200 |
haftmann |
uniform treatment of trivial unit instances: simplify by default, unfold in code preprocessor
|
changeset |
files
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
adapted examples to changes in SMT triggers
|
changeset |
files
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
reduces Sledgehammer dependencies
|
changeset |
files
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
eliminate dependency of SMT2 module on 'list'
|
changeset |
files
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
removed subsumed record-related code, now that records are registered as 'ctr_sugar'
|
changeset |
files
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
made lookup more robust in the face of missing (dummy) case constant
|
changeset |
files
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
use 'ctr_sugar' abstraction in SMT(2)
|
changeset |
files
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
register record extensions as freely generated types
|
changeset |
files
|
| Wed, 11 Jun 2014 18:22:05 +0200 |
haftmann |
mixin definitions are within scope of "for"s of import expression
|
changeset |
files
|
| Wed, 11 Jun 2014 18:22:04 +0200 |
haftmann |
proper proof context transfer wrt. background theory avoids ad-hoc restore operation
|
changeset |
files
|
| Wed, 11 Jun 2014 19:32:39 +0200 |
blanchet |
refactoring
|
changeset |
files
|
| Wed, 11 Jun 2014 19:32:12 +0200 |
blanchet |
moved generic code further up
|
changeset |
files
|
| Wed, 11 Jun 2014 19:15:55 +0200 |
blanchet |
tuned code
|
changeset |
files
|
| Wed, 11 Jun 2014 19:15:54 +0200 |
blanchet |
factor out SMT-LIB 2 type/term parsing from Z3-specific code
|
changeset |
files
|
| Wed, 11 Jun 2014 19:08:32 +0200 |
blanchet |
simplify slightly ATP proof generated for Z3
|
changeset |
files
|
| Wed, 11 Jun 2014 16:02:10 +0200 |
steckerm |
tuned whitespaces
|
changeset |
files
|
| Wed, 11 Jun 2014 15:44:09 +0200 |
blanchet |
updated contributors to include students
|
changeset |
files
|
| Wed, 11 Jun 2014 15:29:23 +0200 |
blanchet |
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
|
changeset |
files
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
adapted SMT examples to new, corrected handling of 'typedef'
|
changeset |
files
|
| 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
|
changeset |
files
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
updated NEWS slightly
|
changeset |
files
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
updated docs w.r.t. Z3
|
changeset |
files
|
| 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
|
changeset |
files
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
removed '_new' sufffix in SMT2 solver names (in some cases)
|
changeset |
files
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
removed old SMT module from Sledgehammer
|
changeset |
files
|
| Wed, 11 Jun 2014 08:58:42 +0200 |
blanchet |
got rid of 'listF' example, which is now subsumed by the real 'list' type
|
changeset |
files
|
| Tue, 10 Jun 2014 21:15:57 +0200 |
blanchet |
changed syntax of map: and rel: arguments to BNF-based datatypes
|
changeset |
files
|
| Tue, 10 Jun 2014 19:51:00 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 10 Jun 2014 19:15:15 +0200 |
blanchet |
updated Z3 certificates
|
changeset |
files
|
| Tue, 10 Jun 2014 19:15:14 +0200 |
blanchet |
generate ':named' attributes in SMT-LIB 2 problems, to facilitate reconstruction
|
changeset |
files
|
| Tue, 10 Jun 2014 19:15:14 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 10 Jun 2014 18:24:53 +0200 |
Andreas Lochbihler |
add type class instances for unit
|
changeset |
files
|
| Tue, 10 Jun 2014 12:16:22 +0200 |
blanchet |
use 'where' clause for selector default value syntax
|
changeset |
files
|
| Tue, 10 Jun 2014 11:38:53 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 09 Jun 2014 16:08:30 +0200 |
nipkow |
added List.union
|
changeset |
files
|
| Mon, 09 Jun 2014 12:36:22 +0200 |
nipkow |
Sup/Inf on functions decoupled from complete_lattice.
|
changeset |
files
|
| Sun, 08 Jun 2014 23:30:53 +0200 |
haftmann |
tuned data structure
|
changeset |
files
|
| Sun, 08 Jun 2014 23:30:52 +0200 |
haftmann |
recovered level-free fishing for locale, accidentally lost in dce365931721
|
changeset |
files
|
| Sun, 08 Jun 2014 23:30:52 +0200 |
haftmann |
tuned terminology: emphasize stack-like nature of nested local theories
|
changeset |
files
|
| Sun, 08 Jun 2014 23:30:51 +0200 |
haftmann |
self-contained locale_declaration operation
|
changeset |
files
|
| 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
|
changeset |
files
|
| Sun, 08 Jun 2014 23:30:50 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sun, 08 Jun 2014 23:30:49 +0200 |
haftmann |
recovered structure of module, which got somehow convoluted due to incremental modifications
|
changeset |
files
|
| 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
|
changeset |
files
|
| 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
|
changeset |
files
|
| 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;
|
changeset |
files
|
| Sat, 07 Jun 2014 21:49:17 +0200 |
haftmann |
treat non-canonical interpretations of classes the same way as ordinary locale interpretations
|
changeset |
files
|
| Sat, 07 Jun 2014 08:16:03 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sat, 07 Jun 2014 08:16:03 +0200 |
haftmann |
avoid odd Named_Target.reinit altogether
|
changeset |
files
|
| 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
|
changeset |
files
|
| Sat, 07 Jun 2014 08:16:03 +0200 |
haftmann |
less baroque interface
|
changeset |
files
|
| Fri, 06 Jun 2014 19:19:46 +0200 |
haftmann |
dropped obscure and unused ad-hoc before_exit hook for named targets
|
changeset |
files
|
| Fri, 06 Jun 2014 12:36:06 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Thu, 05 Jun 2014 14:37:44 +0200 |
noschinl |
mira: USER_HOME must exist for building JEdit documentation
|
changeset |
files
|
| Fri, 06 Jun 2014 10:53:33 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
| Thu, 05 Jun 2014 19:39:38 +0200 |
haftmann |
sharpened criterion: bare named target is only at the bottom level
|
changeset |
files
|
| Thu, 05 Jun 2014 19:39:35 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 05 Jun 2014 11:41:38 +0200 |
traytel |
extended stream library
|
changeset |
files
|
| Thu, 05 Jun 2014 11:11:41 +0200 |
haftmann |
be more explicit: made sml/nj happy
|
changeset |
files
|
| Thu, 05 Jun 2014 10:52:19 +0200 |
haftmann |
always refine interpretation morphism using canonical constant's definition theorem
|
changeset |
files
|
| Wed, 04 Jun 2014 15:32:25 +0200 |
noschinl |
set USER_HOME to affect also ISABELLE_PATH et al
|
changeset |
files
|
| Tue, 03 Jun 2014 16:27:31 +0200 |
blanchet |
merge
|
changeset |
files
|
| Tue, 03 Jun 2014 16:22:59 +0200 |
blanchet |
updated SMT2 certificates
|
changeset |
files
|
| Tue, 03 Jun 2014 16:02:42 +0200 |
blanchet |
tune
|
changeset |
files
|
| Tue, 03 Jun 2014 16:02:41 +0200 |
blanchet |
disable hard-to-reconstruct Z3 feature
|
changeset |
files
|
| Tue, 03 Jun 2014 14:38:41 +0200 |
blanchet |
new Z3 4.3.2 component, based on more recent repository version, and whose Mac binary was built on Mac OS X 10.7
|
changeset |
files
|
| Tue, 03 Jun 2014 16:22:01 +0200 |
hoelzl |
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
|
changeset |
files
|
| Tue, 03 Jun 2014 11:43:07 +0200 |
blanchet |
removed SMT weights -- their impact was very inconclusive anyway
|
changeset |
files
|
| Tue, 03 Jun 2014 10:35:51 +0200 |
blanchet |
make SMT code less dependent on Z3 proofs
|
changeset |
files
|
| Tue, 03 Jun 2014 10:13:44 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 02 Jun 2014 22:38:46 +0200 |
blanchet |
avoid division by 0
|
changeset |
files
|
| Mon, 02 Jun 2014 19:21:41 +0200 |
haftmann |
formal treatment of dangling parameters for class abbrevs analogously to class consts
|
changeset |
files
|
| Mon, 02 Jun 2014 19:21:40 +0200 |
haftmann |
explicit passing of params
|
changeset |
files
|
| Mon, 02 Jun 2014 17:34:27 +0200 |
blanchet |
refactored Z3 to Isar proof construction code
|
changeset |
files
|
| Mon, 02 Jun 2014 17:34:26 +0200 |
blanchet |
simplified counterexample handling
|
changeset |
files
|
| Mon, 02 Jun 2014 17:34:26 +0200 |
blanchet |
split replay and proof parsing for Z3
|
changeset |
files
|
| Mon, 02 Jun 2014 17:34:25 +0200 |
blanchet |
removed counterexample parser (obsolete and useless in practice)
|
changeset |
files
|
| Mon, 02 Jun 2014 16:19:37 +0200 |
hoelzl |
remove superfluous assumption
|
changeset |
files
|
| Mon, 02 Jun 2014 15:10:18 +0200 |
fleury |
basic setup for zipperposition prover
|
changeset |
files
|
| Mon, 02 Jun 2014 14:29:20 +0200 |
desharna |
document property 'sel_set'
|
changeset |
files
|
| Mon, 02 Jun 2014 14:29:20 +0200 |
desharna |
generate 'sel_set' theorem for (co)datatypes
|
changeset |
files
|
| Mon, 02 Jun 2014 11:59:51 +0200 |
blanchet |
removed some spurious warnings in new (co)datatype package
|
changeset |
files
|
| Mon, 02 Jun 2014 11:59:50 +0200 |
blanchet |
add option to keep duplicates, for more precise evaluation of relevance filters
|
changeset |
files
|
| Mon, 02 Jun 2014 11:59:49 +0200 |
blanchet |
tuned whitespace
|
changeset |
files
|
| Sun, 01 Jun 2014 14:00:58 +0200 |
haftmann |
definition in class: provide explicit auxiliary abbreviation carrying potential mixfix syntax in presence of dangling parameters
|
changeset |
files
|
| Sun, 01 Jun 2014 08:33:35 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sat, 31 May 2014 23:00:13 +0200 |
boehmes |
merged
|
changeset |
files
|
| Sat, 31 May 2014 22:59:54 +0200 |
boehmes |
tuned
|
changeset |
files
|
| Sat, 31 May 2014 22:31:03 +0200 |
boehmes |
more complete proof replay for Z3: support universally quantified rewrite steps
|
changeset |
files
|
| Sat, 31 May 2014 09:35:12 +0200 |
haftmann |
postpone const declarations for nested context after canonical const declarations: keep const declarations stemming from interpretation together
|
changeset |
files
|
| Sat, 31 May 2014 09:35:10 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sat, 31 May 2014 09:35:09 +0200 |
haftmann |
explicit is better than implicit
|
changeset |
files
|
| Sat, 31 May 2014 09:35:08 +0200 |
haftmann |
tuned names
|
changeset |
files
|
| Sat, 31 May 2014 09:35:07 +0200 |
haftmann |
dropped accidental duplicate application of morphism
|
changeset |
files
|
| Fri, 30 May 2014 18:48:05 +0200 |
hoelzl |
generalizd measurability on restricted space; rule for integrability on compact sets
|
changeset |
files
|
| Fri, 30 May 2014 15:56:30 +0200 |
hoelzl |
better support for restrict_space
|
changeset |
files
|
| Fri, 30 May 2014 18:13:40 +0200 |
nipkow |
must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
|
changeset |
files
|
| Fri, 30 May 2014 16:10:57 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 30 May 2014 15:34:14 +0200 |
wenzelm |
updated cygwin -- include perl_vendor for libwww-perl;
|
changeset |
files
|
| Fri, 30 May 2014 16:00:54 +0200 |
blanchet |
made 'Kuehlwein-style' be really like Python code, we now think
|
changeset |
files
|
| Fri, 30 May 2014 15:15:41 +0200 |
blanchet |
make SML code closer to Python code when 'nb_kuehlwein_style' is true
|
changeset |
files
|
| Fri, 30 May 2014 15:15:02 +0200 |
blanchet |
merge
|
changeset |
files
|
| Fri, 30 May 2014 14:43:06 +0200 |
blanchet |
added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away
|
changeset |
files
|
| Fri, 30 May 2014 14:55:10 +0200 |
hoelzl |
introduce more powerful reindexing rules for big operators
|
changeset |
files
|
| Fri, 30 May 2014 12:54:42 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 30 May 2014 11:02:02 +0200 |
wenzelm |
make double-sure that old popup is dismissed, before replacing it;
|
changeset |
files
|
| Fri, 30 May 2014 10:50:57 +0200 |
wenzelm |
more robust bold_style, e.g. relevant for accidental \<^bold> before keyword;
|
changeset |
files
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
added another way of invoking Python code, for experiments
|
changeset |
files
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
make SML naive Bayes closer to Python version
|
changeset |
files
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
tuned whitespace, to make datatype definitions slightly less intimidating
|
changeset |
files
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
more work on exporter
|
changeset |
files
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
got rid of 'linearize' option
|
changeset |
files
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
extend exporter with new versions of MaSh
|
changeset |
files
|
| Fri, 30 May 2014 08:23:08 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 30 May 2014 08:23:07 +0200 |
haftmann |
tuned signature
|
changeset |
files
|
| Fri, 30 May 2014 08:23:07 +0200 |
haftmann |
terminating code equations
|
changeset |
files
|
| Thu, 29 May 2014 22:46:21 +0200 |
haftmann |
more direct passing of right-hand side
|
changeset |
files
|
| Thu, 29 May 2014 22:46:20 +0200 |
haftmann |
even more uniform treatment of result after 95e5a633a18f
|
changeset |
files
|