| Fri, 04 Nov 2011 17:19:33 +0100 |
wenzelm |
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
|
changeset |
files
|
| Fri, 04 Nov 2011 15:05:59 +0000 |
blanchet |
document new experimental provers
|
changeset |
files
|
| Fri, 04 Nov 2011 15:05:58 +0000 |
blanchet |
added remote iProver(-Eq) for experimentation
|
changeset |
files
|
| Fri, 04 Nov 2011 13:52:19 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 04 Nov 2011 08:19:24 +0100 |
huffman |
ex/Tree23.thy: automate proof of gfull_add
|
changeset |
files
|
| Fri, 04 Nov 2011 08:00:48 +0100 |
huffman |
ex/Tree23.thy: simplify proof of bal_del0
|
changeset |
files
|
| Fri, 04 Nov 2011 07:37:37 +0100 |
huffman |
ex/Tree23.thy: simplify proof of bal_add0
|
changeset |
files
|
| Fri, 04 Nov 2011 07:04:34 +0100 |
huffman |
ex/Tree23.thy: simpler definition of ordered-ness predicate
|
changeset |
files
|
| Thu, 03 Nov 2011 17:40:50 +0100 |
huffman |
ex/Tree23.thy: prove that deletion preserves balance
|
changeset |
files
|
| Fri, 04 Nov 2011 00:07:45 +0100 |
wenzelm |
more liberal Parse.fixes, to avoid overlap of mixfix with is-pattern (notably in 'obtain' syntax);
|
changeset |
files
|
| Thu, 03 Nov 2011 23:55:53 +0100 |
wenzelm |
more general Proof_Context.bind_propp, which allows outer parameters;
|
changeset |
files
|
| Thu, 03 Nov 2011 23:32:31 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Thu, 03 Nov 2011 22:51:37 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 03 Nov 2011 22:23:41 +0100 |
wenzelm |
tuned signature -- canonical argument order;
|
changeset |
files
|
| Thu, 03 Nov 2011 22:15:47 +0100 |
wenzelm |
tuned -- Variable.declare_term is already part of Variable.auto_fixes;
|
changeset |
files
|
| Thu, 03 Nov 2011 11:18:06 +0100 |
huffman |
ex/Tree23.thy: prove that insertion preserves tree balance and order
|
changeset |
files
|
| Thu, 03 Nov 2011 18:10:47 +1100 |
kleing |
more IMP fragments
|
changeset |
files
|
| Thu, 03 Nov 2011 18:10:13 +1100 |
kleing |
string -> vname
|
changeset |
files
|
| Thu, 03 Nov 2011 16:22:29 +1100 |
kleing |
JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
|
changeset |
files
|
| Thu, 03 Nov 2011 15:54:19 +1100 |
kleing |
more IMP text fragments
|
changeset |
files
|
| Thu, 03 Nov 2011 10:29:05 +1100 |
kleing |
moved latex generation for HOL-IMP out of distribution
|
changeset |
files
|
| Tue, 01 Nov 2011 10:05:28 +0100 |
bulwahn |
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
|
changeset |
files
|
| Mon, 31 Oct 2011 19:12:41 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Mon, 31 Oct 2011 18:29:25 +0100 |
bulwahn |
more robust, declarative and unsurprising computation of types in the quotient type definition
|
changeset |
files
|
| Mon, 31 Oct 2011 17:51:01 +0100 |
blanchet |
improve handling of bound type variables (esp. for TFF1)
|
changeset |
files
|
| Mon, 31 Oct 2011 17:51:01 +0100 |
blanchet |
improved TFF1 output
|
changeset |
files
|
| Mon, 31 Oct 2011 08:50:35 +0100 |
bulwahn |
clarified signature
|
changeset |
files
|
| Mon, 31 Oct 2011 08:43:21 +0100 |
bulwahn |
tuned
|
changeset |
files
|
| Mon, 31 Oct 2011 08:22:56 +0100 |
bulwahn |
tuned
|
changeset |
files
|
| Sun, 30 Oct 2011 22:35:18 +0100 |
wenzelm |
even more uniform Local_Theory.declaration for locales (cf. 57def0b39696, aa35859c8741);
|
changeset |
files
|
| Sun, 30 Oct 2011 22:20:45 +0100 |
wenzelm |
removed obsolete argument (cf. aa35859c8741);
|
changeset |
files
|
| Sun, 30 Oct 2011 09:42:13 +0100 |
huffman |
removed ad-hoc simp rules sin_cos_eq[symmetric], minus_sin_cos_eq[symmetric], cos_sin_eq[symmetric]
|
changeset |
files
|
| Sun, 30 Oct 2011 09:07:02 +0100 |
huffman |
extend cancellation simproc patterns to cover terms like '- (2 * pi) < pi'
|
changeset |
files
|
| Sun, 30 Oct 2011 07:08:33 +0100 |
huffman |
merged
|
changeset |
files
|
| Sat, 29 Oct 2011 10:00:35 +0200 |
huffman |
remove unused function
|
changeset |
files
|
| Sat, 29 Oct 2011 13:51:35 +0200 |
blanchet |
also export DFG formats
|
changeset |
files
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
|
changeset |
files
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added DFG unsorted support (like in the old days)
|
changeset |
files
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
gracefully do nothing if the SPASS input file is already in DFG format
|
changeset |
files
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added sorted DFG output for coming version of SPASS
|
changeset |
files
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9
|
changeset |
files
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
check "sound" flag before doing something unsound...
|
changeset |
files
|
| Sat, 29 Oct 2011 12:57:43 +0200 |
wenzelm |
uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
|
changeset |
files
|
| Sat, 29 Oct 2011 12:55:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Oct 2011 16:49:15 +0200 |
huffman |
more accurate class constraints on cancellation simproc patterns
|
changeset |
files
|
| Sat, 29 Oct 2011 00:23:58 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
changeset |
files
|
| Fri, 28 Oct 2011 23:16:50 +0200 |
wenzelm |
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
|
changeset |
files
|
| Fri, 28 Oct 2011 23:10:44 +0200 |
wenzelm |
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
|
changeset |
files
|
| Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
changeset |
files
|
| Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
changeset |
files
|
| Fri, 28 Oct 2011 15:38:41 +0200 |
wenzelm |
slightly more explicit/syntactic modelling of morphisms;
|
changeset |
files
|
| Fri, 28 Oct 2011 14:10:19 +0200 |
hoelzl |
correct import path
|
changeset |
files
|
| Fri, 28 Oct 2011 14:06:06 +0200 |
hoelzl |
allow to build Probability and MV-Analysis with one ROOT.ML
|
changeset |
files
|
| Fri, 28 Oct 2011 12:37:18 +0200 |
bulwahn |
removing dead code
|
changeset |
files
|
| Fri, 28 Oct 2011 10:33:23 +0200 |
huffman |
ex/Simproc_Tests.thy: remove duplicate simprocs
|
changeset |
files
|
| Fri, 28 Oct 2011 11:02:27 +0200 |
huffman |
use simproc_setup for cancellation simprocs, to get proper name bindings
|
changeset |
files
|
| Thu, 27 Oct 2011 22:37:19 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 27 Oct 2011 22:20:55 +0200 |
wenzelm |
eliminated aliases of standard functions;
|
changeset |
files
|
| Thu, 27 Oct 2011 21:52:57 +0200 |
wenzelm |
more standard attribute setup;
|
changeset |
files
|
| Thu, 27 Oct 2011 21:02:10 +0200 |
wenzelm |
localized quotient data;
|
changeset |
files
|
| Thu, 27 Oct 2011 20:26:38 +0200 |
wenzelm |
simplified/standardized signatures;
|
changeset |
files
|
| Thu, 27 Oct 2011 19:41:08 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 27 Oct 2011 16:28:34 +0200 |
nipkow |
uses IMP and hence requires its tex setup
|
changeset |
files
|
| Thu, 27 Oct 2011 15:59:33 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 27 Oct 2011 15:59:25 +0200 |
nipkow |
tuned text
|
changeset |
files
|
| Thu, 27 Oct 2011 13:52:31 +0200 |
bulwahn |
respecting isabelle's programming style in the quotient package by simplifying qconsts_lookup function for data access; removing odd NotFound exception
|
changeset |
files
|
| Thu, 27 Oct 2011 13:50:55 +0200 |
bulwahn |
respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access
|
changeset |
files
|
| Thu, 27 Oct 2011 13:50:54 +0200 |
bulwahn |
respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access
|
changeset |
files
|
| Thu, 27 Oct 2011 07:48:07 +0200 |
huffman |
merged
|
changeset |
files
|
| Thu, 27 Oct 2011 07:46:57 +0200 |
huffman |
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
|
changeset |
files
|
| Wed, 26 Oct 2011 22:51:06 +0200 |
wenzelm |
more robust ML pretty printing (cf. b6c527c64789);
|
changeset |
files
|
| Wed, 26 Oct 2011 22:50:40 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 25 Oct 2011 16:37:11 +0200 |
bulwahn |
renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library
|
changeset |
files
|
| Tue, 25 Oct 2011 16:09:02 +0200 |
nipkow |
tuned text
|
changeset |
files
|
| Tue, 25 Oct 2011 15:59:15 +0200 |
nipkow |
tuned names to avoid shadowing
|
changeset |
files
|
| Tue, 25 Oct 2011 12:00:52 +0200 |
huffman |
merge Gcd/GCD and Lcm/LCM
|
changeset |
files
|
| Tue, 25 Oct 2011 08:48:36 +0200 |
boehmes |
clarify types of terms: use proper set type
|
changeset |
files
|
| Mon, 24 Oct 2011 16:47:24 +0200 |
huffman |
instance bool :: linorder
|
changeset |
files
|
| Mon, 24 Oct 2011 12:26:05 +0200 |
bulwahn |
removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes
|
changeset |
files
|
| Mon, 24 Oct 2011 11:40:31 +0200 |
bulwahn |
fixed typo
|
changeset |
files
|
| Mon, 24 Oct 2011 10:45:54 +0200 |
nipkow |
latex output not needed because errors manifest themselves earlier
|
changeset |
files
|
| Sun, 23 Oct 2011 23:11:53 +0200 |
wenzelm |
some text on inner-syntax;
|
changeset |
files
|
| Sun, 23 Oct 2011 16:03:59 +0200 |
nipkow |
renamed in ASM
|
changeset |
files
|
| Sun, 23 Oct 2011 14:15:24 +0200 |
nipkow |
tuned order of eqns
|
changeset |
files
|
| Sun, 23 Oct 2011 14:03:37 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Sun, 23 Oct 2011 17:37:21 +1100 |
kleing |
script for exporting filtered IMP files as tar.gz
|
changeset |
files
|
| Sun, 23 Oct 2011 17:12:14 +1100 |
kleing |
removed Norbert's email from isatest (bounces)
|
changeset |
files
|
| Sat, 22 Oct 2011 23:43:01 +0200 |
wenzelm |
class Lexicon as abstract datatype;
|
changeset |
files
|
| Sat, 22 Oct 2011 23:30:02 +0200 |
wenzelm |
more private stuff;
|
changeset |
files
|
| Sat, 22 Oct 2011 23:29:44 +0200 |
wenzelm |
class Text.Edit as abstract datatype;
|
changeset |
files
|
| Sat, 22 Oct 2011 23:29:11 +0200 |
wenzelm |
class Time as abstract datatype;
|
changeset |
files
|
| Sat, 22 Oct 2011 23:28:24 +0200 |
wenzelm |
class Volatile as abstract datatype;
|
changeset |
files
|
| Sat, 22 Oct 2011 20:18:01 +0200 |
nipkow |
merged
|
changeset |
files
|
| Sat, 22 Oct 2011 20:17:50 +0200 |
nipkow |
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
|
changeset |
files
|
| Sat, 22 Oct 2011 19:22:13 +0200 |
wenzelm |
experimental support for Scala 2.9.1.final;
|
changeset |
files
|
| Sat, 22 Oct 2011 19:15:32 +0200 |
wenzelm |
class Path as abstract datatype;
|
changeset |
files
|
| Sat, 22 Oct 2011 19:00:03 +0200 |
wenzelm |
class Counter as abstract datatype;
|
changeset |
files
|
| Sat, 22 Oct 2011 16:57:24 +0200 |
wenzelm |
discontinued redundant ASCII syntax;
|
changeset |
files
|
| Sat, 22 Oct 2011 16:44:34 +0200 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Fri, 21 Oct 2011 22:44:55 +0200 |
wenzelm |
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
|
changeset |
files
|
| Fri, 21 Oct 2011 17:39:07 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 21 Oct 2011 17:39:00 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Fri, 21 Oct 2011 16:21:12 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 21 Oct 2011 14:25:38 +0200 |
bulwahn |
replacing metis proofs with facts xt1 by new proof with more readable names
|
changeset |
files
|
| Fri, 21 Oct 2011 14:06:15 +0200 |
blanchet |
more robust parsing of TSTP sources -- Vampire has nonstandard "introduced()" tags and Waldmeister(OnTPTP) has weird "theory(...)" dependencies
|
changeset |
files
|
| Fri, 21 Oct 2011 12:44:20 +0200 |
blanchet |
disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction
|
changeset |
files
|
| Fri, 21 Oct 2011 11:17:16 +0200 |
bulwahn |
NEWS
|
changeset |
files
|
| Fri, 21 Oct 2011 11:17:15 +0200 |
bulwahn |
updating documentation: code_inline -> code_unfold; added documentation about attribute code_unfold_post
|
changeset |
files
|
| Fri, 21 Oct 2011 11:17:14 +0200 |
bulwahn |
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
|
changeset |
files
|
| Fri, 21 Oct 2011 11:17:12 +0200 |
bulwahn |
removing redundant attribute code_inline in the code generator
|
changeset |
files
|
| Fri, 21 Oct 2011 11:27:21 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 21 Oct 2011 11:26:14 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 21 Oct 2011 10:37:03 +0200 |
bulwahn |
improving mutabelle script again after missing some changes in f4896c792316
|
changeset |
files
|
| Fri, 21 Oct 2011 10:32:42 +0200 |
bulwahn |
correcting code_prolog
|
changeset |
files
|
| Fri, 21 Oct 2011 09:51:45 +0200 |
huffman |
merged
|
changeset |
files
|
| Fri, 21 Oct 2011 08:42:11 +0200 |
huffman |
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
|
changeset |
files
|
| Fri, 21 Oct 2011 08:25:04 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 21 Oct 2011 08:24:57 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 20 Oct 2011 22:26:02 +0200 |
blanchet |
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
|
changeset |
files
|
| Thu, 20 Oct 2011 22:02:49 +0200 |
huffman |
merged
|
changeset |
files
|
| Thu, 20 Oct 2011 17:27:14 +0200 |
huffman |
removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)
|
changeset |
files
|
| Thu, 20 Oct 2011 12:30:43 -0400 |
kleing |
removed [trans] concept from basic material
|
changeset |
files
|
| Thu, 20 Oct 2011 10:44:00 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 20 Oct 2011 10:43:47 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 20 Oct 2011 09:59:12 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Thu, 20 Oct 2011 09:11:13 +0200 |
bulwahn |
modernizing predicate_compile_quickcheck
|
changeset |
files
|
| Thu, 20 Oct 2011 08:20:35 +0200 |
bulwahn |
adding depth as an quickcheck configuration
|
changeset |
files
|
| Thu, 20 Oct 2011 09:48:00 +0200 |
nipkow |
renamed name -> vname
|
changeset |
files
|
| Wed, 19 Oct 2011 23:07:48 +0200 |
haftmann |
removed some remaining artefacts of ancient SML code generator
|
changeset |
files
|
| Wed, 19 Oct 2011 22:54:26 +0200 |
haftmann |
NEWS
|
changeset |
files
|
| Wed, 19 Oct 2011 21:40:32 +0200 |
blanchet |
cleaner LEO-II extensionality step detection
|
changeset |
files
|
| Wed, 19 Oct 2011 21:40:32 +0200 |
blanchet |
marginally cleaner proof parsing, that doesn't stumble upon LEO-II's E-step proofs
|
changeset |
files
|
| Wed, 19 Oct 2011 21:40:32 +0200 |
blanchet |
one more LEO-II failure
|
changeset |
files
|
| Wed, 19 Oct 2011 19:45:19 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 19 Oct 2011 17:45:25 +0200 |
huffman |
merged
|
changeset |
files
|
| Tue, 18 Oct 2011 15:19:06 +0200 |
huffman |
hide typedef-generated constants Product_Type.prod and Sum_Type.sum
|
changeset |
files
|
| Wed, 19 Oct 2011 16:36:13 +0200 |
blanchet |
more uniform SZS status handling
|
changeset |
files
|
| Wed, 19 Oct 2011 16:36:13 +0200 |
blanchet |
avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"
|
changeset |
files
|
| Wed, 19 Oct 2011 16:32:30 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 19 Oct 2011 16:32:12 +0200 |
nipkow |
renamed B to Bc
|
changeset |
files
|
| Wed, 19 Oct 2011 17:04:43 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Wed, 19 Oct 2011 17:03:07 +0200 |
wenzelm |
proper source positions for @{lemma};
|
changeset |
files
|
| Wed, 19 Oct 2011 16:45:46 +0200 |
wenzelm |
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
|
changeset |
files
|
| Wed, 19 Oct 2011 15:42:43 +0200 |
wenzelm |
inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
|
changeset |
files
|
| Wed, 19 Oct 2011 15:41:12 +0200 |
wenzelm |
tuned legacy signature;
|
changeset |
files
|
| Wed, 19 Oct 2011 14:40:49 +0200 |
wenzelm |
further cleanup of stats (cf. 97e81a8aa277);
|
changeset |
files
|
| Wed, 19 Oct 2011 14:22:06 +0200 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Wed, 19 Oct 2011 14:21:29 +0200 |
wenzelm |
really document just one code generator;
|
changeset |
files
|
| Wed, 19 Oct 2011 09:11:21 +0200 |
bulwahn |
NEWS
|
changeset |
files
|
| Wed, 19 Oct 2011 09:11:20 +0200 |
bulwahn |
removing old code generator
|
changeset |
files
|
| Wed, 19 Oct 2011 09:11:19 +0200 |
bulwahn |
removing declaration of code_unfold to address the old code generator
|
changeset |
files
|
| Wed, 19 Oct 2011 09:11:18 +0200 |
bulwahn |
removing dependency of the generic code generator to old code generator functions thyname_of_type and thyname_of_const
|
changeset |
files
|
| Wed, 19 Oct 2011 09:11:18 +0200 |
bulwahn |
removing documentation about the old code generator
|
changeset |
files
|
| Wed, 19 Oct 2011 09:11:16 +0200 |
bulwahn |
removing old code generator setup for executable sets
|
changeset |
files
|
| Wed, 19 Oct 2011 09:11:15 +0200 |
bulwahn |
removing old code generator setup for efficient natural numbers; cleaned typo
|
changeset |
files
|
| Wed, 19 Oct 2011 09:11:14 +0200 |
bulwahn |
removing old code generator setup for real numbers; tuned
|
changeset |
files
|
| Wed, 19 Oct 2011 09:11:14 +0200 |
bulwahn |
removing old code generator setup for rational numbers; tuned
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:29 +0200 |
bulwahn |
removing old code generator setup for strings
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:27 +0200 |
bulwahn |
removing old code generator setup for lists
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:26 +0200 |
bulwahn |
removing old code generator setup for integers
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:25 +0200 |
bulwahn |
removing old code generator for inductive predicates
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:24 +0200 |
bulwahn |
removing quickcheck tester SML-inductive based on the old code generator
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:23 +0200 |
bulwahn |
removing old code generator setup for inductive sets in the inductive set package
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:22 +0200 |
bulwahn |
removing old code generator setup of inductive predicates
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:21 +0200 |
bulwahn |
removing old code generator setup for product types
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:20 +0200 |
bulwahn |
removing old code generator setup for function types
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:19 +0200 |
bulwahn |
removing old code generator setup for datatypes
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:17 +0200 |
bulwahn |
removing old code generator for recursive functions
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:16 +0200 |
bulwahn |
removing old code generator setup in the HOL theory
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:15 +0200 |
bulwahn |
removing invocations of the evaluation method based on the old code generator
|
changeset |
files
|
| Wed, 19 Oct 2011 08:37:14 +0200 |
bulwahn |
removing invocations of the old code generator
|
changeset |
files
|
| Tue, 18 Oct 2011 15:40:59 +0200 |
blanchet |
freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing
|
changeset |
files
|
| Tue, 18 Oct 2011 15:40:58 +0200 |
blanchet |
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
|
changeset |
files
|
| Tue, 18 Oct 2011 15:27:18 +0200 |
bulwahn |
tuned
|
changeset |
files
|
| Tue, 18 Oct 2011 15:27:17 +0200 |
bulwahn |
adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra
|
changeset |
files
|
| Tue, 18 Oct 2011 11:59:03 +0200 |
krauss |
mira: collect size of heap images
|
changeset |
files
|
| Mon, 17 Oct 2011 21:37:38 +0200 |
blanchet |
updated doc related to Satallax
|
changeset |
files
|
| Mon, 17 Oct 2011 21:37:37 +0200 |
blanchet |
parse Satallax unsat cores
|
changeset |
files
|
| Mon, 17 Oct 2011 18:05:14 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 17 Oct 2011 14:22:14 +0200 |
noschinl |
(old) NEWS
|
changeset |
files
|
| Mon, 17 Oct 2011 10:19:01 +0200 |
bulwahn |
moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
|
changeset |
files
|
| Mon, 17 Oct 2011 11:24:22 +0200 |
wenzelm |
always use sockets on Windows/Cygwin;
|
changeset |
files
|
| Sun, 16 Oct 2011 21:49:47 +0200 |
krauss |
mira configuration: use official polyml 5.4.1 on lxbroy10
|
changeset |
files
|
| Sun, 16 Oct 2011 18:48:30 +0200 |
wenzelm |
added Term.dummy_pattern conveniences;
|
changeset |
files
|
| Sun, 16 Oct 2011 16:56:01 +0200 |
wenzelm |
slightly more standard-conformant XML parsing (see also 94033767ef9b);
|
changeset |
files
|
| Sun, 16 Oct 2011 14:48:01 +0200 |
haftmann |
tuned proof
|
changeset |
files
|
| Sun, 16 Oct 2011 14:48:00 +0200 |
haftmann |
tuned type annnotation
|
changeset |
files
|
| Sun, 16 Oct 2011 14:48:00 +0200 |
haftmann |
hide not_member as also member
|
changeset |
files
|
| Sat, 15 Oct 2011 20:40:13 +0200 |
wenzelm |
misc tuning and modernization;
|
changeset |
files
|
| Sat, 15 Oct 2011 18:14:36 +0200 |
wenzelm |
updated to Scala 2.8.2.final;
|
changeset |
files
|
| Sat, 15 Oct 2011 17:00:17 +0200 |
wenzelm |
prefer recent polyml-5.4.1, but retain potentially fragile polyml-5.2.1 as experimental test;
|
changeset |
files
|
| Sat, 15 Oct 2011 16:58:37 +0200 |
wenzelm |
updated to polyml-5.4.1;
|
changeset |
files
|
| Sat, 15 Oct 2011 15:55:10 +0200 |
wenzelm |
updated to polyml-5.4.1;
|
changeset |
files
|
| Sat, 15 Oct 2011 00:18:00 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 14 Oct 2011 22:42:56 +0200 |
haftmann |
monadic bind
|
changeset |
files
|
| Fri, 14 Oct 2011 18:55:59 +0200 |
haftmann |
moved sublists to More_List.thy
|
changeset |
files
|
| Fri, 14 Oct 2011 18:55:29 +0200 |
haftmann |
NEWS
|
changeset |
files
|
| Fri, 14 Oct 2011 11:34:30 +0200 |
wenzelm |
more complete stats, including small sessions which provide some clues on main HOL baseline performance;
|
changeset |
files
|
| Thu, 13 Oct 2011 23:35:15 +0200 |
haftmann |
avoid very specific code equation for card; corrected spelling
|
changeset |
files
|
| Thu, 13 Oct 2011 23:27:46 +0200 |
haftmann |
bouned transitive closure
|
changeset |
files
|
| Thu, 13 Oct 2011 23:02:59 +0200 |
haftmann |
moved acyclic predicate up in hierarchy
|
changeset |
files
|
| Thu, 13 Oct 2011 22:56:19 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 13 Oct 2011 22:56:19 +0200 |
haftmann |
modernized definitions
|
changeset |
files
|
| Thu, 13 Oct 2011 22:50:35 +0200 |
wenzelm |
static dummy_task (again) to avoid a few extra allocations;
|
changeset |
files
|
| Thu, 13 Oct 2011 13:49:55 +0200 |
noschinl |
tuned markup
|
changeset |
files
|
| Thu, 13 Oct 2011 11:45:33 +0200 |
wenzelm |
discontinued obsolete 'types' command;
|
changeset |
files
|
| Wed, 12 Oct 2011 22:48:23 +0200 |
wenzelm |
modernized structure Induct_Tacs;
|
changeset |
files
|
| Wed, 12 Oct 2011 22:21:38 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 12 Oct 2011 21:39:33 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Wed, 12 Oct 2011 20:57:40 +0200 |
wenzelm |
tuned ML style;
|
changeset |
files
|
| Wed, 12 Oct 2011 20:16:48 +0200 |
wenzelm |
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
|
changeset |
files
|
| Wed, 12 Oct 2011 16:21:07 +0200 |
wenzelm |
discontinued obsolete alias structure ProofContext;
|
changeset |
files
|
| Wed, 12 Oct 2011 09:16:30 +0200 |
nipkow |
separated monotonicity reasoning and defined narrowing with while_option
|
changeset |
files
|
| Mon, 10 Oct 2011 20:14:25 +0200 |
wenzelm |
include no-smlnj targets into library (cf. e54a985daa61);
|
changeset |
files
|
| Mon, 10 Oct 2011 16:47:45 +0200 |
bulwahn |
increasing values_timeout to avoid SML_makeall failures on our current tests
|
changeset |
files
|
| Mon, 10 Oct 2011 11:12:09 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 10 Oct 2011 11:10:45 +0200 |
wenzelm |
removed obsolete RC tags;
|
changeset |
files
|
| Sun, 09 Oct 2011 11:13:53 +0200 |
huffman |
Int.thy: discontinued some legacy theorems
|
changeset |
files
|
| Sun, 09 Oct 2011 08:30:48 +0200 |
huffman |
Set.thy: remove redundant [simp] declarations
|
changeset |
files
|
| Mon, 03 Oct 2011 22:21:19 +0200 |
bulwahn |
removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
|
changeset |
files
|
| Mon, 03 Oct 2011 15:39:30 +0200 |
bulwahn |
tune text for document generation
|
changeset |
files
|
| Mon, 03 Oct 2011 14:43:15 +0200 |
bulwahn |
adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
|
changeset |
files
|
| Mon, 03 Oct 2011 14:43:14 +0200 |
bulwahn |
adding code equations for cardinality and (reflexive) transitive closure on finite types
|
changeset |
files
|
| Mon, 03 Oct 2011 14:43:13 +0200 |
bulwahn |
adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure
|
changeset |
files
|
| Mon, 03 Oct 2011 14:43:12 +0200 |
bulwahn |
adding lemma to List library for executable equation of the (refl) transitive closure
|
changeset |
files
|
| Thu, 29 Sep 2011 21:42:03 +0200 |
Jean Pichon |
fixed typos in IMP
|
changeset |
files
|
| Wed, 28 Sep 2011 10:35:56 +0200 |
nipkow |
added nice interval syntax
|
changeset |
files
|
| Wed, 28 Sep 2011 09:59:55 +0200 |
nipkow |
Added dependecies
|
changeset |
files
|
| Wed, 28 Sep 2011 09:55:11 +0200 |
nipkow |
Added Hoare-like Abstract Interpretation
|
changeset |
files
|
| Wed, 28 Sep 2011 08:51:55 +0200 |
nipkow |
moved IMP/AbsInt stuff into subdirectory Abs_Int_Den
|
changeset |
files
|
| Mon, 26 Sep 2011 21:13:26 +0200 |
wenzelm |
back to post-release mode;
|
changeset |
files
|
| Sun, 09 Oct 2011 17:06:19 +0200 |
wenzelm |
Added tag Isabelle2011-1 for changeset 76fef3e57004
|
changeset |
files
|
| Sun, 09 Oct 2011 16:47:58 +0200 |
wenzelm |
tuned;
Isabelle2011-1
|
changeset |
files
|
| Sun, 09 Oct 2011 15:46:06 +0200 |
wenzelm |
updated ISABELLE_HOME_USER;
|
changeset |
files
|
| Tue, 04 Oct 2011 14:51:51 +0200 |
wenzelm |
more explicit check of Java executable -- relevant for Linux x86/x86_64 mismatch and absence on Mac OS Lion;
|
changeset |
files
|
| Mon, 03 Oct 2011 11:16:51 +0200 |
wenzelm |
Added tag Isabelle2011-1-RC2 for changeset a45121ffcfcb
|
changeset |
files
|
| Mon, 03 Oct 2011 11:14:19 +0200 |
wenzelm |
some amendments due to Jean Pichon;
|
changeset |
files
|
| Thu, 29 Sep 2011 09:37:59 +0200 |
traytel |
correct coercion generation in case of unknown map functions
|
changeset |
files
|
| Wed, 28 Sep 2011 13:52:14 +0200 |
wenzelm |
proper platform_file_url for Windows UNC paths (server shares);
|
changeset |
files
|
| Tue, 27 Sep 2011 22:35:57 +0200 |
wenzelm |
proper platform_file_url;
|
changeset |
files
|
| Tue, 27 Sep 2011 22:14:15 +0200 |
wenzelm |
observe base URL of rendered document;
|
changeset |
files
|
| Tue, 27 Sep 2011 21:39:55 +0200 |
wenzelm |
more README;
|
changeset |
files
|
| Tue, 27 Sep 2011 20:45:15 +0200 |
wenzelm |
tuned README.html;
|
changeset |
files
|
| Tue, 27 Sep 2011 20:25:15 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 27 Sep 2011 14:17:40 +0200 |
wenzelm |
retain output, which is required for non-existent JRE, for example (cf. b455e4f42c04);
|
changeset |
files
|
| Tue, 27 Sep 2011 00:03:11 +0200 |
wenzelm |
tuned message, which is displayed after termination of Isabelle.app on Mac OS;
|
changeset |
files
|
| Mon, 26 Sep 2011 23:51:59 +0200 |
wenzelm |
keep top-level "Isabelle" executable -- now an alias for "isabelle jedit";
|
changeset |
files
|
| Mon, 26 Sep 2011 23:43:52 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 26 Sep 2011 21:41:39 +0200 |
wenzelm |
ensure Isabelle env;
|
changeset |
files
|
| Mon, 26 Sep 2011 21:17:25 +0200 |
wenzelm |
Added tag Isabelle2011-1-RC1 for changeset 24ad77c3a147
|
changeset |
files
|
| Mon, 26 Sep 2011 21:09:28 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 26 Sep 2011 20:53:53 +0200 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
| Mon, 26 Sep 2011 20:39:18 +0200 |
wenzelm |
reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;
|
changeset |
files
|
| Mon, 26 Sep 2011 20:31:41 +0200 |
wenzelm |
makedist for release;
|
changeset |
files
|
| Mon, 26 Sep 2011 14:03:43 +0200 |
blanchet |
put MiniSat back first -- Torlak's eval seemed to suggest that Crypto and Lingeling were better, but Crypto is slower on "Nitpick_Examples" and Crypto crashes
|
changeset |
files
|
| Mon, 26 Sep 2011 11:41:52 +0200 |
blanchet |
require Java 1.6 in the Nitpick documentation -- technically 1.5 will also work with Kodkodi 1.2.16, but it won't work with Kodkodi 1.5.0
|
changeset |
files
|
| Mon, 26 Sep 2011 11:41:52 +0200 |
blanchet |
put CryptoMiniSat first and remove warning about unsoundness now that it has been fixed in Kodkod
|
changeset |
files
|
| Mon, 26 Sep 2011 10:57:20 +0200 |
bulwahn |
adding an example with inductive predicates to quickcheck narrowing examples
|
changeset |
files
|
| Mon, 26 Sep 2011 10:30:37 +0200 |
bulwahn |
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
|
changeset |
files
|
| Sun, 25 Sep 2011 19:34:20 +0200 |
blanchet |
clarify platforms
|
changeset |
files
|
| Sun, 25 Sep 2011 18:43:25 +0200 |
blanchet |
killed JNI version of zChaff, since Kodkod 1.5 does not support it anymore
|
changeset |
files
|
| Sun, 25 Sep 2011 18:43:25 +0200 |
blanchet |
updated Nitpick SAT Solver doc
|
changeset |
files
|
| Sun, 25 Sep 2011 18:43:25 +0200 |
blanchet |
update list of SAT solvers reflecting Kodkod 1.5
|
changeset |
files
|
| Sun, 25 Sep 2011 17:25:34 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 25 Sep 2011 13:48:59 +0200 |
wenzelm |
more uniform defaults;
|
changeset |
files
|
| Sun, 25 Sep 2011 09:37:33 +0200 |
haftmann |
Quotient_Set.thy is part of library
|
changeset |
files
|
| Sun, 25 Sep 2011 00:32:49 +0200 |
nipkow |
fixed typo
|
changeset |
files
|
| Sat, 24 Sep 2011 17:18:39 +0200 |
wenzelm |
standardize drive letters -- important for proper document node identification;
|
changeset |
files
|
| Sat, 24 Sep 2011 10:45:57 +0200 |
wenzelm |
more user aliases;
|
changeset |
files
|
| Sat, 24 Sep 2011 00:17:32 +0100 |
sultana |
fixed IsaMakefile action for HOL-TPTP.
|
changeset |
files
|
| Fri, 23 Sep 2011 23:46:13 +0200 |
wenzelm |
prefer socket comminication on Cygwin, which is more stable here than fifos;
|
changeset |
files
|
| Fri, 23 Sep 2011 21:51:49 +0200 |
wenzelm |
tuned proof;
|
changeset |
files
|
| Fri, 23 Sep 2011 17:35:06 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Fri, 23 Sep 2011 17:23:54 +0200 |
wenzelm |
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
|
changeset |
files
|
| Fri, 23 Sep 2011 17:11:08 +0200 |
wenzelm |
updated header;
|
changeset |
files
|
| Fri, 23 Sep 2011 16:50:39 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Fri, 23 Sep 2011 16:44:51 +0200 |
blanchet |
reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)
|
changeset |
files
|
| Fri, 23 Sep 2011 14:25:53 +0200 |
blanchet |
first step towards extending Minipick with more translations
|
changeset |
files
|
| Fri, 23 Sep 2011 14:08:50 +0200 |
berghofe |
Include keywords print_coercions and print_coercion_maps
|
changeset |
files
|
| Wed, 17 Aug 2011 19:49:07 +0200 |
traytel |
local coercion insertion algorithm to support complex coercions
|
changeset |
files
|
| Wed, 17 Aug 2011 19:49:07 +0200 |
traytel |
printing and deleting of coercions
|
changeset |
files
|
| Fri, 23 Sep 2011 14:59:29 +0200 |
wenzelm |
raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;
|
changeset |
files
|
| Fri, 23 Sep 2011 14:13:15 +0200 |
wenzelm |
default print mode for Isabelle/Scala, not just Isabelle/jEdit;
|
changeset |
files
|
| Fri, 23 Sep 2011 14:12:09 +0200 |
wenzelm |
augment existing print mode;
|
changeset |
files
|
| Fri, 23 Sep 2011 13:44:31 +0200 |
wenzelm |
explicit option for socket vs. fifo communication;
|
changeset |
files
|
| Fri, 23 Sep 2011 13:43:44 +0200 |
wenzelm |
tuned proof;
|
changeset |
files
|
| Fri, 23 Sep 2011 10:31:12 +0200 |
blanchet |
synchronized section names with manual
|
changeset |
files
|
| Fri, 23 Sep 2011 00:11:29 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Thu, 22 Sep 2011 14:12:16 -0700 |
huffman |
discontinued legacy theorem names from RealDef.thy
|
changeset |
files
|
| Thu, 22 Sep 2011 13:17:14 -0700 |
huffman |
merged
|
changeset |
files
|
| Thu, 22 Sep 2011 12:55:19 -0700 |
huffman |
discontinued HOLCF legacy theorem names
|
changeset |
files
|
| Thu, 22 Sep 2011 19:42:06 +0200 |
blanchet |
take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime
|
changeset |
files
|
| Thu, 22 Sep 2011 18:23:38 +0200 |
berghofe |
Moved extraction part of Higman's lemma to separate theory to allow reuse in
|
changeset |
files
|
| Thu, 22 Sep 2011 17:15:46 +0200 |
berghofe |
Removed hcentering and vcentering options, since they are not supported
|
changeset |
files
|
| Thu, 22 Sep 2011 16:56:19 +0200 |
berghofe |
merged
|
changeset |
files
|
| Thu, 22 Sep 2011 16:50:23 +0200 |
berghofe |
Added documentation for HOL-SPARK
|
changeset |
files
|
| Thu, 22 Sep 2011 16:30:47 +0200 |
blanchet |
drop partial monomorphic instances in Metis, like in Sledgehammer
|
changeset |
files
|
| Thu, 22 Sep 2011 16:30:47 +0200 |
blanchet |
better type reconstruction -- prevents ill-instantiations in proof replay
|
changeset |
files
|
| Thu, 22 Sep 2011 10:02:16 -0400 |
hoelzl |
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
|
changeset |
files
|
| Thu, 22 Sep 2011 10:48:53 +0200 |
bulwahn |
changing quickcheck_timeout to 30 seconds in mutabelle's testing
|
changeset |
files
|
| Thu, 22 Sep 2011 07:26:53 +0200 |
bulwahn |
adding post-processing of terms to narrowing-based Quickcheck
|
changeset |
files
|
| Wed, 21 Sep 2011 17:43:13 -0700 |
huffman |
HOL/ex/ROOT.ML: only list BinEx once
|
changeset |
files
|
| Wed, 21 Sep 2011 10:59:55 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 21 Sep 2011 08:28:53 -0700 |
huffman |
remove redundant instantiation ereal :: power
|
changeset |
files
|
| Wed, 21 Sep 2011 15:55:16 +0200 |
blanchet |
reintroduced Minipick as Nitpick example
|
changeset |
files
|
| Wed, 21 Sep 2011 15:55:15 +0200 |
blanchet |
tuned comment
|
changeset |
files
|
| Wed, 21 Sep 2011 06:41:34 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 20 Sep 2011 11:02:41 -0700 |
huffman |
Extended_Real_Limits: generalize some lemmas
|
changeset |
files
|
| Tue, 20 Sep 2011 10:52:08 -0700 |
huffman |
add lemmas within_empty and tendsto_bot;
|
changeset |
files
|
| Thu, 22 Sep 2011 21:58:05 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Thu, 22 Sep 2011 20:33:08 +0200 |
wenzelm |
abstract System_Channel in ML (cf. Scala version);
|
changeset |
files
|
| Wed, 21 Sep 2011 22:18:17 +0200 |
wenzelm |
alternative Socket_Channel;
|
changeset |
files
|
| Wed, 21 Sep 2011 20:35:50 +0200 |
wenzelm |
more abstract wrapping of fifos as System_Channel;
|
changeset |
files
|
| Wed, 21 Sep 2011 17:50:25 +0200 |
wenzelm |
slightly more general Socket_IO as part of Pure;
|
changeset |
files
|
| Wed, 21 Sep 2011 16:04:29 +0200 |
wenzelm |
more hints on Z3 configuration;
|
changeset |
files
|
| Wed, 21 Sep 2011 15:08:15 +0200 |
wenzelm |
reduced default thread stack, to increase the success rate especially on Windows (NB: the actor worker farm tends to produce 100-200 threads for big sessions);
|
changeset |
files
|
| Wed, 21 Sep 2011 07:31:08 +0200 |
nipkow |
renamed inv -> filter
|
changeset |
files
|
| Wed, 21 Sep 2011 07:04:04 +0200 |
nipkow |
Added proofs about narowing
|
changeset |
files
|
| Wed, 21 Sep 2011 07:03:16 +0200 |
nipkow |
added missing makefile dependence
|
changeset |
files
|
| Wed, 21 Sep 2011 06:26:15 +0200 |
nipkow |
added example
|
changeset |
files
|
| Wed, 21 Sep 2011 03:24:54 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Wed, 21 Sep 2011 02:38:53 +0200 |
nipkow |
refined comment
|
changeset |
files
|
| Wed, 21 Sep 2011 09:17:01 +1000 |
kleing |
fixed two typos in IMP (by Jean Pichon)
|
changeset |
files
|
| Wed, 21 Sep 2011 00:12:36 +0200 |
nipkow |
merged
|
changeset |
files
|
| Tue, 20 Sep 2011 05:48:23 +0200 |
nipkow |
Updated IMP to use new induction method
|
changeset |
files
|
| Tue, 20 Sep 2011 05:47:11 +0200 |
nipkow |
New proof method "induction" that gives induction hypotheses the name IH.
|
changeset |
files
|
| Tue, 20 Sep 2011 22:11:22 +0200 |
haftmann |
official status for UN_singleton
|
changeset |
files
|
| Tue, 20 Sep 2011 21:47:52 +0200 |
haftmann |
tuned specification and lemma distribution among theories; tuned proofs
|
changeset |
files
|
| Tue, 20 Sep 2011 15:23:17 +0200 |
wenzelm |
more careful treatment of initial update, similar to output panel;
|
changeset |
files
|
| Tue, 20 Sep 2011 15:07:30 +0200 |
wenzelm |
proper fact binding;
|
changeset |
files
|
| Tue, 20 Sep 2011 09:30:19 +0200 |
bulwahn |
syntactic improvements and tuning names in the code generator due to Florian's code review
|
changeset |
files
|
| Tue, 20 Sep 2011 01:32:04 +0200 |
krauss |
match types when applying mono_thm -- previous export generalizes type variables;
|
changeset |
files
|
| Mon, 19 Sep 2011 23:34:22 +0200 |
wenzelm |
fixed headers;
|
changeset |
files
|
| Mon, 19 Sep 2011 23:24:32 +0200 |
wenzelm |
less ambiguous syntax;
|
changeset |
files
|
| Mon, 19 Sep 2011 23:18:18 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 19 Sep 2011 22:48:05 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 19 Sep 2011 16:18:34 +0200 |
bulwahn |
catch PatternMatchFail exceptions in narrowing-based quickcheck
|
changeset |
files
|
| Mon, 19 Sep 2011 16:18:33 +0200 |
bulwahn |
removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition
|
changeset |
files
|
| Mon, 19 Sep 2011 16:18:30 +0200 |
bulwahn |
ensuring that some constants are generated in the source code by adding calls in ensure_testable
|
changeset |
files
|
| Mon, 19 Sep 2011 16:18:23 +0200 |
bulwahn |
adding abstraction layer; more precise function names
|
changeset |
files
|
| Mon, 19 Sep 2011 16:18:21 +0200 |
bulwahn |
adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used
|
changeset |
files
|
| Mon, 19 Sep 2011 16:18:19 +0200 |
bulwahn |
determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations
|
changeset |
files
|
| Mon, 19 Sep 2011 16:18:19 +0200 |
bulwahn |
only annotating constants with sort constraints
|
changeset |
files
|
| Mon, 19 Sep 2011 16:18:18 +0200 |
bulwahn |
also adding type annotations for the dynamic invocation
|
changeset |
files
|
| Mon, 19 Sep 2011 14:35:51 +0200 |
noschinl |
removed legacy lemmas in Complete_Lattices
|
changeset |
files
|
| Mon, 19 Sep 2011 14:24:53 +0200 |
bulwahn |
increasing quickcheck timeout to reduce spurious test failures due to massive parallel invocations and bad scheduling
|
changeset |
files
|
| Mon, 19 Sep 2011 22:45:57 +0200 |
wenzelm |
more isatest stats;
|
changeset |
files
|
| Mon, 19 Sep 2011 22:42:57 +0200 |
wenzelm |
refined Symbol.is_symbolic -- cover recoded versions as well;
|
changeset |
files
|
| Mon, 19 Sep 2011 22:13:51 +0200 |
wenzelm |
double clicks switch to document node buffer;
|
changeset |
files
|
| Mon, 19 Sep 2011 21:53:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 19 Sep 2011 21:41:48 +0200 |
wenzelm |
explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
|
changeset |
files
|
| Mon, 19 Sep 2011 16:40:17 +0200 |
wenzelm |
at least 2 worker threads to ensure some degree of lifeness, notably for asynchronous Document.print_state;
|
changeset |
files
|
| Mon, 19 Sep 2011 14:40:38 +0200 |
wenzelm |
instantaneous cleanup (NB: VIEWER should be synchronous, cf. dd25b3055c4e);
|
changeset |
files
|
| Mon, 19 Sep 2011 14:31:20 +0200 |
wenzelm |
unique file names via serial numbers, to allow files like "root" or multiple files with same base name;
|
changeset |
files
|
| Mon, 19 Sep 2011 12:58:52 +0200 |
wenzelm |
imitate Apple in setting initial shell PATH -- especially relevant for MacTeX, MacPorts etc.;
|
changeset |
files
|
| Sun, 18 Sep 2011 16:12:43 -0700 |
huffman |
merged
|
changeset |
files
|
| Thu, 15 Sep 2011 10:12:36 -0700 |
huffman |
numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else
|
changeset |
files
|
| Sun, 18 Sep 2011 21:41:36 +0200 |
wenzelm |
removed obsolete patches for PG 4.1;
|
changeset |
files
|
| Sun, 18 Sep 2011 21:15:31 +0200 |
wenzelm |
additional space for borderless UI;
|
changeset |
files
|
| Sun, 18 Sep 2011 20:26:08 +0200 |
wenzelm |
more robust treatment of empty insets (NB: border may be null on some UIs, e.g. Windows);
|
changeset |
files
|
| Sun, 18 Sep 2011 19:49:35 +0200 |
wenzelm |
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
|
changeset |
files
|
| Sun, 18 Sep 2011 16:33:30 +0200 |
wenzelm |
isatest settings for macbroy6 (Mac OS X Lion);
|
changeset |
files
|
| Sun, 18 Sep 2011 16:24:26 +0200 |
wenzelm |
more Mac OS reference hardware;
|
changeset |
files
|
| Sun, 18 Sep 2011 16:11:26 +0200 |
wenzelm |
updated to SML/NJ 110.73;
|
changeset |
files
|
| Sun, 18 Sep 2011 15:59:38 +0200 |
wenzelm |
tentative announcement based on current NEWS;
|
changeset |
files
|
| Sun, 18 Sep 2011 15:57:36 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 18 Sep 2011 15:39:55 +0200 |
wenzelm |
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
|
changeset |
files
|
| Sun, 18 Sep 2011 15:30:31 +0200 |
wenzelm |
updated for release;
|
changeset |
files
|
| Sun, 18 Sep 2011 15:30:21 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 18 Sep 2011 14:55:45 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Sun, 18 Sep 2011 14:55:27 +0200 |
wenzelm |
updated Complete_Lattices;
|
changeset |
files
|
| Sun, 18 Sep 2011 14:48:25 +0200 |
wenzelm |
some tuning and re-ordering for release;
|
changeset |
files
|
| Sun, 18 Sep 2011 14:34:24 +0200 |
wenzelm |
misc tuning for release;
|
changeset |
files
|
| Sun, 18 Sep 2011 14:25:53 +0200 |
wenzelm |
more contributors;
|
changeset |
files
|
| Sun, 18 Sep 2011 14:09:57 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Sun, 18 Sep 2011 13:56:06 +0200 |
wenzelm |
tweak keyboard shortcuts for Mac OS X;
|
changeset |
files
|
| Sun, 18 Sep 2011 13:47:12 +0200 |
wenzelm |
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
|
changeset |
files
|
| Sun, 18 Sep 2011 13:39:33 +0200 |
wenzelm |
finite sequences as useful as introductory example;
|
changeset |
files
|
| Sun, 18 Sep 2011 12:48:45 +0200 |
wenzelm |
discontinued hard-wired JAVA_HOME treatment for Mac OS X (cf. f471a2fb9a95), which can cause confusions of "isabelle java" vs. "isabelle scala" -- moved settings to external component;
|
changeset |
files
|
| Sun, 18 Sep 2011 00:05:22 +0200 |
wenzelm |
graph traversal in topological order;
|
changeset |
files
|
| Sat, 17 Sep 2011 23:04:03 +0200 |
wenzelm |
Document.Node.Name convenience;
|
changeset |
files
|
| Sat, 17 Sep 2011 22:13:15 +0200 |
wenzelm |
more precise painting;
|
changeset |
files
|
| Sat, 17 Sep 2011 21:28:52 +0200 |
wenzelm |
more elaborate Node_Renderer, which paints node_name.theory only;
|
changeset |
files
|
| Sat, 17 Sep 2011 19:55:32 +0200 |
wenzelm |
raised default log level -- to avoid confusing warning about scala.tools.nsc.plugins.Plugin, which is mistaken as jEdit plugin;
|
changeset |
files
|
| Sat, 17 Sep 2011 19:44:58 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 17 Sep 2011 19:25:14 +0200 |
wenzelm |
more careful traversal of theory dependencies to retain standard import order;
|
changeset |
files
|
| Sat, 17 Sep 2011 17:55:39 +0200 |
wenzelm |
sane default for class Thy_Load;
|
changeset |
files
|
| Sat, 17 Sep 2011 17:05:31 +0200 |
wenzelm |
removed obsolete patches for PG 4.1;
|
changeset |
files
|
| Sat, 17 Sep 2011 16:53:01 +0200 |
wenzelm |
specific bundle for x86_64-linux, which is especially important for JRE due to its extra library dependencies;
|
changeset |
files
|
| Sat, 17 Sep 2011 16:29:18 +0200 |
wenzelm |
added "isabelle scalac" convenience;
|
changeset |
files
|
| Sat, 17 Sep 2011 16:19:40 +0200 |
wenzelm |
Symbol.explode as in ML;
|
changeset |
files
|
| Sat, 17 Sep 2011 16:00:54 +0200 |
wenzelm |
ignore OUTPUT to avoid spam -- jEdit menu "Troubleshooting / Activity Log" should be sufficient;
|
changeset |
files
|
| Sat, 17 Sep 2011 15:08:55 +0200 |
haftmann |
dropped unused argument – avoids problem with SML/NJ
|
changeset |
files
|
| Sat, 17 Sep 2011 00:40:27 +0200 |
haftmann |
tuned spacing
|
changeset |
files
|
| Sat, 17 Sep 2011 00:37:21 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sat, 17 Sep 2011 04:41:44 +0200 |
nipkow |
tuned post fixpoint setup
|
changeset |
files
|
| Sat, 17 Sep 2011 03:37:14 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 16 Sep 2011 09:18:15 +0200 |
nipkow |
when applying induction rules, remove names of assumptions that come
|
changeset |
files
|
| Fri, 16 Sep 2011 20:08:29 +0200 |
noschinl |
remove stray "using [[simp_trace]]"
|
changeset |
files
|
| Fri, 16 Sep 2011 20:02:35 +0200 |
noschinl |
tune indenting
|
changeset |
files
|
| Fri, 16 Sep 2011 12:10:43 +1000 |
kleing |
removed unused legacy lemma names, some comment cleanup.
|
changeset |
files
|
| Fri, 16 Sep 2011 12:10:15 +1000 |
kleing |
removed word_neq_0_conv from simpset, it's almost never wanted.
|
changeset |
files
|
| Thu, 15 Sep 2011 12:40:08 -0400 |
hoelzl |
removed further legacy rules from Complete_Lattices
|
changeset |
files
|
| Thu, 15 Sep 2011 17:06:00 +0200 |
noschinl |
NEWS on Complete_Lattices, Lattices
|
changeset |
files
|
| Thu, 15 Sep 2011 10:57:40 +0200 |
blanchet |
tail recursive proof preprocessing (needed for huge proofs)
|
changeset |
files
|
| Thu, 15 Sep 2011 10:57:40 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 15 Sep 2011 09:44:27 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 15 Sep 2011 09:44:08 +0200 |
nipkow |
revised AbsInt and added widening and narrowing
|
changeset |
files
|
| Wed, 14 Sep 2011 23:47:04 +0200 |
haftmann |
updated comment
|
changeset |
files
|
| Wed, 14 Sep 2011 23:46:02 +0200 |
haftmann |
updated generated code
|
changeset |
files
|
| Tue, 13 Sep 2011 07:56:46 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
changeset |
files
|
| Wed, 14 Sep 2011 10:55:07 +0200 |
noschinl |
merged
|
changeset |
files
|
| Wed, 14 Sep 2011 10:24:22 +0200 |
noschinl |
create central list for language extensions used by the haskell code generator
|
changeset |
files
|
| Wed, 14 Sep 2011 09:46:59 +0200 |
boehmes |
observe distinction between sets and predicates
|
changeset |
files
|
| Wed, 14 Sep 2011 06:49:24 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 14 Sep 2011 06:49:01 +0200 |
nipkow |
cleand up AbsInt fixpoint iteration; tuned syntax
|
changeset |
files
|
| Tue, 13 Sep 2011 17:25:19 -0700 |
huffman |
tuned proofs
|
changeset |
files
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
changeset |
files
|
| Tue, 13 Sep 2011 08:21:51 -0700 |
huffman |
remove some redundant [simp] declarations;
|
changeset |
files
|
| Tue, 13 Sep 2011 16:22:01 +0200 |
noschinl |
tune proofs
|
changeset |
files
|
| Tue, 13 Sep 2011 16:21:48 +0200 |
noschinl |
tune simpset for Complete_Lattices
|
changeset |
files
|
| Tue, 13 Sep 2011 13:17:52 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Tue, 13 Sep 2011 12:14:29 +0200 |
bulwahn |
added lemma motivated by a more specific lemma in the AFP-KBPs theories
|
changeset |
files
|
| Tue, 13 Sep 2011 11:24:58 +0200 |
blanchet |
simplified unsound proof detection by removing impossible case
|
changeset |
files
|
| Tue, 13 Sep 2011 09:56:38 +0200 |
bulwahn |
correcting NEWS
|
changeset |
files
|
| Tue, 13 Sep 2011 09:28:03 +0200 |
bulwahn |
correcting theory name and dependencies
|
changeset |
files
|
| Tue, 13 Sep 2011 09:25:19 +0200 |
bulwahn |
renamed AList_Impl to AList
|
changeset |
files
|
| Tue, 13 Sep 2011 07:13:49 +0200 |
nipkow |
fastsimp -> fastforce in doc
|
changeset |
files
|
| Mon, 12 Sep 2011 14:49:34 -0700 |
huffman |
fix typo
|
changeset |
files
|
| Mon, 12 Sep 2011 14:39:10 -0700 |
huffman |
shorten proof of frontier_straddle
|
changeset |
files
|
| Mon, 12 Sep 2011 13:19:10 -0700 |
huffman |
NEWS and CONTRIBUTORS
|
changeset |
files
|
| Mon, 12 Sep 2011 11:54:20 -0700 |
huffman |
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
|
changeset |
files
|
| Mon, 12 Sep 2011 11:39:29 -0700 |
huffman |
simplify proofs using LIMSEQ lemmas
|
changeset |
files
|
| Mon, 12 Sep 2011 10:43:36 -0700 |
huffman |
remove trivial lemma Lim_at_iff_LIM
|
changeset |
files
|
| Mon, 12 Sep 2011 10:28:45 -0700 |
huffman |
fix typos
|
changeset |
files
|
| Mon, 12 Sep 2011 09:37:49 -0700 |
huffman |
NEWS for euclidean_space class
|
changeset |
files
|
| Mon, 12 Sep 2011 09:21:01 -0700 |
huffman |
move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
|
changeset |
files
|
| Mon, 12 Sep 2011 09:57:33 -0400 |
hoelzl |
adding NEWS and CONTRIBUTORS
|
changeset |
files
|
| Mon, 12 Sep 2011 13:35:35 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Mon, 12 Sep 2011 12:33:37 +0200 |
bulwahn |
correcting imports after splitting and renaming AssocList
|
changeset |
files
|
| Mon, 12 Sep 2011 10:59:38 +0200 |
bulwahn |
tuned
|
changeset |
files
|
| Mon, 12 Sep 2011 10:57:58 +0200 |
bulwahn |
moving connection of association lists to Mappings into a separate theory
|
changeset |
files
|
| Mon, 12 Sep 2011 10:27:36 +0200 |
bulwahn |
adding NEWS and CONTRIBUTORS
|
changeset |
files
|
| Mon, 12 Sep 2011 09:45:53 +0200 |
bulwahn |
tuned some symbol that probably went there by some strange encoding issue
|
changeset |
files
|
| Mon, 12 Sep 2011 11:05:32 +0200 |
blanchet |
added my contributions to NEWS and CONTRIBUTORS
|
changeset |
files
|
| Mon, 12 Sep 2011 10:49:37 +0200 |
blanchet |
fixed type intersection (again)
|
changeset |
files
|
| Mon, 12 Sep 2011 10:49:37 +0200 |
blanchet |
consistent option naming
|
changeset |
files
|
| Mon, 12 Sep 2011 09:07:23 +0200 |
nipkow |
NEWS fastsimp -> fastforce
|
changeset |
files
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
changeset |
files
|
| Sun, 11 Sep 2011 22:56:05 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 11 Sep 2011 13:49:42 -0700 |
huffman |
NEWS for Library/Product_Lattice.thy
|
changeset |
files
|
| Sun, 11 Sep 2011 22:55:26 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sun, 11 Sep 2011 21:35:35 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 11 Sep 2011 10:30:50 -0700 |
huffman |
merged
|
changeset |
files
|
| Sun, 11 Sep 2011 09:40:18 -0700 |
huffman |
tuned proofs
|
changeset |
files
|
| Sun, 11 Sep 2011 07:21:45 -0700 |
huffman |
Library/Saturated.thy: 'Sat' abbreviates 'of_nat'
|
changeset |
files
|
| Sun, 11 Sep 2011 21:34:23 +0200 |
wenzelm |
more CONTRIBUTORS;
|
changeset |
files
|
| Sun, 11 Sep 2011 20:19:20 +0200 |
wenzelm |
persistent ISABELLE_INTERFACE_CHOICE;
|
changeset |
files
|
| Sun, 11 Sep 2011 19:52:09 +0200 |
wenzelm |
explicit choice of interface;
|
changeset |
files
|
| Sun, 11 Sep 2011 17:30:01 +0200 |
wenzelm |
more orthogonal signature;
|
changeset |
files
|
| Sun, 11 Sep 2011 15:20:09 +0200 |
wenzelm |
updates for release;
|
changeset |
files
|
| Sun, 11 Sep 2011 14:58:52 +0200 |
wenzelm |
misc tuning and clarification (NB: settings are already local for named snapshots/releases);
|
changeset |
files
|
| Sun, 11 Sep 2011 14:42:15 +0200 |
wenzelm |
some updates of PLATFORMS;
|
changeset |
files
|
| Sun, 11 Sep 2011 13:27:22 +0200 |
wenzelm |
more README;
|
changeset |
files
|
| Sat, 10 Sep 2011 23:28:58 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 10 Sep 2011 22:43:17 +0200 |
krauss |
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
|
changeset |
files
|
| Sat, 10 Sep 2011 23:27:32 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sat, 10 Sep 2011 22:11:55 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sat, 10 Sep 2011 21:47:55 +0200 |
wenzelm |
speed up slow proof;
|
changeset |
files
|
| Sat, 10 Sep 2011 20:41:27 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 10 Sep 2011 19:44:41 +0200 |
haftmann |
more modularization
|
changeset |
files
|
| Sat, 10 Sep 2011 20:39:13 +0200 |
wenzelm |
stronger colors (as background);
|
changeset |
files
|
| Sat, 10 Sep 2011 20:22:22 +0200 |
wenzelm |
some color scheme for theory status;
|
changeset |
files
|
| Sat, 10 Sep 2011 16:30:08 +0200 |
wenzelm |
some keyboard shortcuts for important actions;
|
changeset |
files
|
| Sat, 10 Sep 2011 14:48:06 +0200 |
wenzelm |
explicit jEdit actions -- to enable key mappings, for example;
|
changeset |
files
|
| Sat, 10 Sep 2011 14:28:07 +0200 |
wenzelm |
more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
|
changeset |
files
|
| Sat, 10 Sep 2011 13:43:09 +0200 |
wenzelm |
tuned usage;
|
changeset |
files
|
| Sat, 10 Sep 2011 13:41:03 +0200 |
wenzelm |
simplified default Isabelle application wrapper (NB: build process is already part of isabelle jedit tool);
|
changeset |
files
|
| Sat, 10 Sep 2011 10:29:24 +0200 |
haftmann |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
|
changeset |
files
|
| Sat, 10 Sep 2011 00:44:25 +0200 |
blanchet |
fixed definition of type intersection (soundness bug)
|
changeset |
files
|
| Sat, 10 Sep 2011 00:44:25 +0200 |
blanchet |
continue with minimization in debug mode in spite of unsoundness
|
changeset |
files
|
| Fri, 09 Sep 2011 09:31:04 -0700 |
huffman |
generalize lemma of_nat_number_of_eq to class number_semiring
|
changeset |
files
|
| Fri, 09 Sep 2011 15:14:59 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Fri, 09 Sep 2011 14:43:50 +0200 |
bulwahn |
stating more explicitly our expectation that these two terms have the same term structure
|
changeset |
files
|
| Fri, 09 Sep 2011 12:33:09 +0200 |
bulwahn |
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
|
changeset |
files
|
| Fri, 09 Sep 2011 14:30:57 +0200 |
blanchet |
made SML/NJ happy
|
changeset |
files
|
| Thu, 08 Sep 2011 12:23:11 +0200 |
noschinl |
call ghc with -XEmptyDataDecls
|
changeset |
files
|
| Fri, 09 Sep 2011 06:47:14 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 09 Sep 2011 06:45:39 +0200 |
nipkow |
tuned headers
|
changeset |
files
|
| Thu, 08 Sep 2011 19:35:23 -0700 |
huffman |
Library/Saturated.thy: number_semiring class instance
|
changeset |
files
|
| Thu, 08 Sep 2011 18:47:23 -0700 |
huffman |
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
|
changeset |
files
|
| Thu, 08 Sep 2011 18:13:48 -0700 |
huffman |
merged
|
changeset |
files
|
| Thu, 08 Sep 2011 10:07:53 -0700 |
huffman |
remove unnecessary intermediate lemmas
|
changeset |
files
|
| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
changeset |
files
|
| Thu, 08 Sep 2011 08:41:28 -0700 |
huffman |
prove existence, uniqueness, and other properties of complex arg function
|
changeset |
files
|
| Thu, 08 Sep 2011 07:27:57 -0700 |
huffman |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 07:16:47 -0700 |
huffman |
remove obsolete intermediate lemma complex_inverse_complex_split
|
changeset |
files
|
| Thu, 08 Sep 2011 07:06:59 -0700 |
huffman |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 11:31:53 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 08 Sep 2011 11:31:23 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 00:35:22 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 08:13:38 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 22:37:32 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 22:04:14 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 07:23:45 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 05 Sep 2011 22:02:32 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Mon, 05 Sep 2011 19:18:38 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 05 Sep 2011 07:49:31 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sun, 04 Sep 2011 09:28:15 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 09:25:55 +0200 |
blanchet |
fixed computation of "in_conj" for polymorphic encodings
|
changeset |
files
|
| Wed, 07 Sep 2011 22:44:26 -0700 |
huffman |
add some new lemmas about cis and rcis;
|
changeset |
files
|
| Wed, 07 Sep 2011 20:44:39 -0700 |
huffman |
Complex.thy: move theorems into appropriate subsections
|
changeset |
files
|
| Wed, 07 Sep 2011 19:24:28 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 17:41:29 -0700 |
huffman |
remove redundant lemma complex_of_real_minus_one
|
changeset |
files
|
| Wed, 07 Sep 2011 18:47:55 -0700 |
huffman |
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
|
changeset |
files
|
| Wed, 07 Sep 2011 10:04:07 -0700 |
huffman |
removed unused lemma sin_cos_squared_add2_mult
|
changeset |
files
|
| Wed, 07 Sep 2011 09:45:39 -0700 |
huffman |
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
|
changeset |
files
|
| Wed, 07 Sep 2011 09:02:58 -0700 |
huffman |
avoid using legacy theorem names
|
changeset |
files
|
| Thu, 08 Sep 2011 00:23:23 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 23:55:40 +0200 |
haftmann |
theory of saturated naturals contributed by Peter Gammie
|
changeset |
files
|
| Wed, 07 Sep 2011 23:38:52 +0200 |
haftmann |
theory of saturated naturals contributed by Peter Gammie
|
changeset |
files
|
| Wed, 07 Sep 2011 23:07:16 +0200 |
haftmann |
lemmas about +, *, min, max on nat
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
update Sledgehammer docs
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
added new tagged encodings to Metis tests
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
also implemented ghost version of the tagged encodings
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
added new guards encoding to test
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
smarter explicit apply business
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
started work on ghost type arg encoding
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
stricted type encoding parsing
|
changeset |
files
|
| Thu, 08 Sep 2011 00:20:09 +0200 |
wenzelm |
more substructural sharing to gain significant compression;
|
changeset |
files
|
| Wed, 07 Sep 2011 23:08:04 +0200 |
wenzelm |
XML.cache for partial sharing (strings only);
|
changeset |
files
|
| Wed, 07 Sep 2011 22:00:41 +0200 |
wenzelm |
platform-specific look and feel;
|
changeset |
files
|
| Wed, 07 Sep 2011 21:41:36 +0200 |
wenzelm |
more README;
|
changeset |
files
|
| Wed, 07 Sep 2011 21:38:48 +0200 |
wenzelm |
clarified terminology;
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:50 +0200 |
wenzelm |
no print_state for final proof commands, which return to theory state;
|
changeset |
files
|
| Wed, 07 Sep 2011 21:10:47 +0200 |
wenzelm |
NEWS on IsabelleText font;
|
changeset |
files
|
| Wed, 07 Sep 2011 21:05:53 +0200 |
wenzelm |
explicit join_syntax ensures command transaction integrity of 'theory';
|
changeset |
files
|
| Wed, 07 Sep 2011 20:49:45 +0200 |
wenzelm |
some updates for release;
|
changeset |
files
|
| Wed, 07 Sep 2011 20:29:54 +0200 |
wenzelm |
some tuning for release;
|
changeset |
files
|
| Wed, 07 Sep 2011 18:01:01 +0200 |
wenzelm |
updated file locations;
|
changeset |
files
|
| Wed, 07 Sep 2011 17:42:57 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 14:58:40 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:39 +0200 |
bulwahn |
removing previously used function locally_monomorphic in the code generator
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:38 +0200 |
bulwahn |
setting const_sorts to false in the type inference of the code generator
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:37 +0200 |
bulwahn |
adapting Imperative HOL serializer to changes of the iterm datatype in the code generator
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:36 +0200 |
bulwahn |
removing previous crude approximation to add type annotations to disambiguate types
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:35 +0200 |
bulwahn |
adding minimalistic implementation for printing the type annotations
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:34 +0200 |
bulwahn |
adding call to disambiguation annotations
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:34 +0200 |
bulwahn |
adding type inference for disambiguation annotations in code equation
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:32 +0200 |
bulwahn |
adding the body type as well to the code generation for constants as it is required for type annotations of constants
|
changeset |
files
|
| Wed, 07 Sep 2011 13:51:30 +0200 |
bulwahn |
changing const type to pass along if typing annotations are necessary for disambigous terms
|
changeset |
files
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
fixed THF type constructor syntax
|
changeset |
files
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tweaking polymorphic TFF and THF output
|
changeset |
files
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
parse new experimental '@' encodings
|
changeset |
files
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 07 Sep 2011 13:50:16 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 07 Sep 2011 17:03:34 +0200 |
wenzelm |
clarified import;
|
changeset |
files
|
| Wed, 07 Sep 2011 16:53:49 +0200 |
wenzelm |
tuned/simplified proofs;
|
changeset |
files
|
| Wed, 07 Sep 2011 16:37:50 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 07 Sep 2011 11:36:39 +0200 |
wenzelm |
deactivate unfinished charset provider for now, to avoid user confusion;
|
changeset |
files
|
| Wed, 07 Sep 2011 11:26:27 +0200 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Wed, 07 Sep 2011 11:17:19 +0200 |
wenzelm |
added "check" button: adhoc change to full buffer perspective;
|
changeset |
files
|
| Wed, 07 Sep 2011 11:00:39 +0200 |
wenzelm |
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
make mangling sound w.r.t. type arguments
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
make "filter_type_args" more robust if the actual arity is higher than the declared one
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
updated Sledgehammer documentation
|
changeset |
files
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
rationalize uniform encodings
|
changeset |
files
|
| Tue, 06 Sep 2011 22:41:35 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 19:03:41 -0700 |
huffman |
avoid using legacy theorem names
|
changeset |
files
|
| Tue, 06 Sep 2011 16:30:39 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 14:53:51 -0700 |
huffman |
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
|
changeset |
files
|
| Wed, 07 Sep 2011 07:59:45 +0900 |
Cezary Kaliszyk |
HOL/Import: Update HOL4 generated files to current Isabelle.
|
changeset |
files
|
| Wed, 07 Sep 2011 00:08:09 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Tue, 06 Sep 2011 13:16:46 -0700 |
huffman |
remove some unnecessary simp rules from simpset
|
changeset |
files
|
| Tue, 06 Sep 2011 21:56:11 +0200 |
wenzelm |
some Isabelle/jEdit NEWS;
|
changeset |
files
|
| Tue, 06 Sep 2011 21:40:58 +0200 |
wenzelm |
more README;
|
changeset |
files
|
| Tue, 06 Sep 2011 21:11:12 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 10:30:33 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 10:30:00 -0700 |
huffman |
simplify proof of tan_half, removing unused assumptions
|
changeset |
files
|
| Tue, 06 Sep 2011 09:56:09 -0700 |
huffman |
convert some proofs to Isar-style
|
changeset |
files
|
| Tue, 06 Sep 2011 18:13:36 +0200 |
blanchet |
added dummy polymorphic THF system
|
changeset |
files
|
| Tue, 06 Sep 2011 18:07:44 +0200 |
boehmes |
added some examples for pattern and weight annotations
|
changeset |
files
|
| Tue, 06 Sep 2011 17:52:00 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 16:40:22 +0200 |
bulwahn |
avoid "Code" as structure name (cf. 3bc39cfe27fe)
|
changeset |
files
|
| Tue, 06 Sep 2011 08:00:28 -0700 |
huffman |
remove duplicate copy of lemma sqrt_add_le_add_sqrt
|
changeset |
files
|
| Tue, 06 Sep 2011 07:48:59 -0700 |
huffman |
remove redundant lemma real_sum_squared_expand in favor of power2_sum
|
changeset |
files
|
| Tue, 06 Sep 2011 07:45:18 -0700 |
huffman |
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
|
changeset |
files
|
| Tue, 06 Sep 2011 07:41:15 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 05 Sep 2011 22:30:25 -0700 |
huffman |
add lemmas about arctan;
|
changeset |
files
|
| Mon, 05 Sep 2011 18:06:02 -0700 |
huffman |
convert lemma cos_total to Isar-style proof
|
changeset |
files
|
| Tue, 06 Sep 2011 14:25:16 +0200 |
nipkow |
added new lemmas
|
changeset |
files
|
| Tue, 06 Sep 2011 11:31:01 +0200 |
blanchet |
updated Sledgehammer's docs
|
changeset |
files
|
| Tue, 06 Sep 2011 11:31:01 +0200 |
blanchet |
cleanup "simple" type encodings
|
changeset |
files
|
| Tue, 06 Sep 2011 17:50:04 +0900 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| Tue, 06 Sep 2011 16:45:31 +0900 |
Cezary Kaliszyk |
HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.
|
changeset |
files
|
| Tue, 06 Sep 2011 09:11:08 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 06 Sep 2011 09:11:08 +0200 |
blanchet |
drop more type arguments soundly, when they can be deduced from the arg types
|
changeset |
files
|
| Tue, 06 Sep 2011 20:55:18 +0200 |
wenzelm |
bulk reports for improved message throughput;
|
changeset |
files
|
| Tue, 06 Sep 2011 20:37:07 +0200 |
wenzelm |
bulk reports for improved message throughput;
|
changeset |
files
|
| Tue, 06 Sep 2011 19:48:57 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 06 Sep 2011 11:25:27 +0200 |
wenzelm |
more specific message channels to avoid potential bottle-neck of raw_messages;
|
changeset |
files
|
| Tue, 06 Sep 2011 11:18:19 +0200 |
wenzelm |
buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
|
changeset |
files
|
| Tue, 06 Sep 2011 10:27:04 +0200 |
wenzelm |
more abstract receiver interface;
|
changeset |
files
|
| Tue, 06 Sep 2011 10:16:12 +0200 |
wenzelm |
flush after Output.raw_message (and init message) for reduced latency of important protocol events;
|
changeset |
files
|
| Mon, 05 Sep 2011 17:45:37 -0700 |
huffman |
convert lemma cos_is_zero to Isar-style
|
changeset |
files
|
| Mon, 05 Sep 2011 17:05:00 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 05 Sep 2011 17:00:56 -0700 |
huffman |
convert lemma sin_gt_zero to Isar style;
|
changeset |
files
|
| Mon, 05 Sep 2011 16:26:57 -0700 |
huffman |
modify lemma sums_group, and shorten proofs that use it
|
changeset |
files
|
| Mon, 05 Sep 2011 16:07:40 -0700 |
huffman |
generalize some lemmas
|
changeset |
files
|
| Mon, 05 Sep 2011 12:19:04 -0700 |
huffman |
add lemmas cos_arctan and sin_arctan
|
changeset |
files
|
| Mon, 05 Sep 2011 08:38:50 -0700 |
huffman |
tuned indentation
|
changeset |
files
|
| Mon, 05 Sep 2011 23:51:16 +0200 |
wenzelm |
more visible outdated_color;
|
changeset |
files
|
| Mon, 05 Sep 2011 23:26:41 +0200 |
wenzelm |
commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
|
changeset |
files
|
| Mon, 05 Sep 2011 20:30:37 +0200 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Mon, 05 Sep 2011 14:42:31 +0200 |
blanchet |
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
|
changeset |
files
|
| Mon, 05 Sep 2011 14:17:44 +0200 |
boehmes |
tuned
|
changeset |
files
|
| Mon, 05 Sep 2011 11:34:54 +0200 |
boehmes |
tuned
|
changeset |
files
|
| Mon, 05 Sep 2011 11:28:10 +0200 |
boehmes |
filter out all schematic theorems if the problem contains no ground constants
|
changeset |
files
|
| Sun, 04 Sep 2011 21:04:02 -0700 |
huffman |
merged
|
changeset |
files
|
| Sun, 04 Sep 2011 21:03:54 -0700 |
huffman |
tuned comments
|
changeset |
files
|
| Sun, 04 Sep 2011 11:16:47 -0700 |
huffman |
simplify proof of Bseq_mono_convergent
|
changeset |
files
|
| Sun, 04 Sep 2011 20:37:20 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 04 Sep 2011 10:29:38 -0700 |
huffman |
replace lemma expi_imaginary with reoriented lemma cis_conv_exp
|
changeset |
files
|
| Sun, 04 Sep 2011 10:05:52 -0700 |
huffman |
remove redundant lemmas expi_add and expi_zero
|
changeset |
files
|
| Sun, 04 Sep 2011 09:49:45 -0700 |
huffman |
remove redundant lemmas about LIMSEQ
|
changeset |
files
|
| Sun, 04 Sep 2011 07:15:13 -0700 |
huffman |
introduce abbreviation 'int' earlier in Int.thy
|
changeset |
files
|
| Sun, 04 Sep 2011 06:56:10 -0700 |
huffman |
remove unused assumptions from natceiling lemmas
|
changeset |
files
|
| Sun, 04 Sep 2011 06:27:59 -0700 |
huffman |
move lemmas nat_le_iff and nat_mono into Int.thy
|
changeset |
files
|
| Sun, 04 Sep 2011 19:36:19 +0200 |
wenzelm |
eliminated markup for plain identifiers (frequent but insignificant);
|
changeset |
files
|
| Sun, 04 Sep 2011 19:12:06 +0200 |
wenzelm |
simplified signatures;
|
changeset |
files
|
| Sun, 04 Sep 2011 19:06:45 +0200 |
wenzelm |
synchronous XML.Cache without actor -- potentially more efficient on machines with few cores;
|
changeset |
files
|
| Sun, 04 Sep 2011 17:50:19 +0200 |
wenzelm |
tuned document;
|
changeset |
files
|
| Sun, 04 Sep 2011 17:35:34 +0200 |
wenzelm |
improved handling of extended styles and hard tabs when prover is inactive;
|
changeset |
files
|
| Sun, 04 Sep 2011 17:21:11 +0200 |
wenzelm |
mark hard tabs as single chunks, as required by jEdit;
|
changeset |
files
|
| Sun, 04 Sep 2011 16:37:22 +0200 |
wenzelm |
updated READMEs;
|
changeset |
files
|
| Sun, 04 Sep 2011 15:49:59 +0200 |
wenzelm |
property "tooltip-dismiss-delay" is edited in ms, not seconds;
|
changeset |
files
|
| Sun, 04 Sep 2011 15:21:50 +0200 |
wenzelm |
moved XML/YXML to src/Pure/PIDE;
|
changeset |
files
|
| Sun, 04 Sep 2011 14:29:15 +0200 |
wenzelm |
pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
|
changeset |
files
|
| Sun, 04 Sep 2011 08:43:06 +0200 |
haftmann |
pseudo-definition for perms on sets; tuned
|
changeset |
files
|
| Sat, 03 Sep 2011 16:00:09 -0700 |
huffman |
remove duplicate lemma nat_zero in favor of nat_0
|
changeset |
files
|
| Sat, 03 Sep 2011 15:37:41 -0700 |
huffman |
merged
|
changeset |
files
|
| Sat, 03 Sep 2011 15:09:51 -0700 |
huffman |
merged
|
changeset |
files
|
| Sat, 03 Sep 2011 14:52:40 -0700 |
huffman |
modify nominal packages to better respect set/pred distinction
|
changeset |
files
|
| Sat, 03 Sep 2011 14:33:45 -0700 |
huffman |
merged
|
changeset |
files
|
| Sat, 03 Sep 2011 11:10:38 -0700 |
huffman |
remove unused assumption from lemma posreal_complete
|
changeset |
files
|
| Sat, 03 Sep 2011 23:59:36 +0200 |
haftmann |
tuned specifications
|
changeset |
files
|
| Sat, 03 Sep 2011 23:38:06 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sat, 03 Sep 2011 17:56:33 +0200 |
haftmann |
tuned proof
|
changeset |
files
|
| Sat, 03 Sep 2011 17:32:45 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sat, 03 Sep 2011 17:32:35 +0200 |
haftmann |
assert Pure equations for theorem references; avoid dynamic reference to fact
|
changeset |
files
|
| Sat, 03 Sep 2011 17:32:34 +0200 |
haftmann |
assert Pure equations for theorem references; tuned
|
changeset |
files
|
| Sat, 03 Sep 2011 17:32:34 +0200 |
haftmann |
tuned specifications and proofs
|
changeset |
files
|
| Sat, 03 Sep 2011 22:11:49 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 03 Sep 2011 09:26:11 -0700 |
huffman |
remove duplicate lemma finite_choice in favor of finite_set_choice
|
changeset |
files
|
| Sat, 03 Sep 2011 09:12:19 -0700 |
huffman |
simplify proof
|
changeset |
files
|
| Sat, 03 Sep 2011 08:01:49 -0700 |
huffman |
shorten some proofs
|
changeset |
files
|
| Fri, 02 Sep 2011 20:58:31 -0700 |
huffman |
remove redundant simp rules ceiling_floor and floor_ceiling
|
changeset |
files
|
| Sat, 03 Sep 2011 22:05:25 +0200 |
wenzelm |
misc tuning and simplification of proofs;
|
changeset |
files
|
| Sat, 03 Sep 2011 21:15:35 +0200 |
wenzelm |
Document.removed_versions on Scala side;
|
changeset |
files
|
| Sat, 03 Sep 2011 19:47:31 +0200 |
wenzelm |
discontinued predefined empty command (obsolete!?);
|
changeset |
files
|
| Sat, 03 Sep 2011 19:39:16 +0200 |
wenzelm |
discontinued global execs: store exec value directly within entries;
|
changeset |
files
|
| Sat, 03 Sep 2011 18:08:09 +0200 |
wenzelm |
Document.remove_versions on ML side;
|
changeset |
files
|
| Sat, 03 Sep 2011 12:31:27 +0200 |
wenzelm |
some support to prune_history;
|
changeset |
files
|
| Fri, 02 Sep 2011 16:58:00 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 02 Sep 2011 16:57:51 -0700 |
huffman |
speed up extremely slow metis proof of Sup_real_iff
|
changeset |
files
|
| Fri, 02 Sep 2011 16:48:30 -0700 |
huffman |
remove redundant lemma reals_complete2 in favor of complete_real
|
changeset |
files
|
| Fri, 02 Sep 2011 15:19:59 -0700 |
huffman |
simplify proof of Rats_dense_in_real;
|
changeset |
files
|
| Fri, 02 Sep 2011 14:27:55 -0700 |
huffman |
remove unused, unnecessary lemmas
|
changeset |
files
|
| Fri, 02 Sep 2011 13:57:12 -0700 |
huffman |
remove more duplicate lemmas
|
changeset |
files
|
| Fri, 02 Sep 2011 23:04:12 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 02 Sep 2011 19:29:48 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 02 Sep 2011 19:29:36 +0200 |
haftmann |
avoid "Code" as structure name
|
changeset |
files
|
| Fri, 02 Sep 2011 22:48:56 +0200 |
wenzelm |
more robust chunk painting wrt. hard tabs, when chunk.str == null;
|
changeset |
files
|
| Fri, 02 Sep 2011 21:48:27 +0200 |
wenzelm |
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
|
changeset |
files
|
| Fri, 02 Sep 2011 21:06:05 +0200 |
wenzelm |
less agressive parsing of commands (priority ~1);
|
changeset |
files
|
| Fri, 02 Sep 2011 20:35:32 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 02 Sep 2011 20:29:39 +0200 |
wenzelm |
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
|
changeset |
files
|
| Fri, 02 Sep 2011 19:25:44 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 02 Sep 2011 19:25:18 +0200 |
nipkow |
Added Abstract Interpretation theories
|
changeset |
files
|
| Fri, 02 Sep 2011 18:17:45 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 02 Sep 2011 17:58:32 +0200 |
wenzelm |
proper config option linarith_trace;
|
changeset |
files
|
| Fri, 02 Sep 2011 17:57:37 +0200 |
wenzelm |
discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;
|
changeset |
files
|
| Fri, 02 Sep 2011 16:20:09 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
|
changeset |
files
|
| Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
use new syntax for Pi binder in TFF1 output
|
changeset |
files
|
| Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
fewer TPTP important messages
|
changeset |
files
|
| Thu, 01 Sep 2011 10:41:19 -0700 |
huffman |
simplify some proofs about uniform continuity, and add some new ones;
|
changeset |
files
|
| Thu, 01 Sep 2011 09:02:14 -0700 |
huffman |
modernize lemmas about 'continuous' and 'continuous_on';
|
changeset |
files
|
| Thu, 01 Sep 2011 07:31:33 -0700 |
huffman |
add lemma tendsto_infnorm
|
changeset |
files
|
| Fri, 02 Sep 2011 15:21:40 +0200 |
wenzelm |
more precise iterate_entries_after if start refers to last entry;
|
changeset |
files
|
| Fri, 02 Sep 2011 11:52:13 +0200 |
wenzelm |
clarified define_command: store name as structural information;
|
changeset |
files
|
| Thu, 01 Sep 2011 23:08:42 +0200 |
wenzelm |
amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
|
changeset |
files
|
| Thu, 01 Sep 2011 22:29:57 +0200 |
wenzelm |
more redable Document.Node.toString;
|
changeset |
files
|
| Thu, 01 Sep 2011 16:58:41 +0200 |
wenzelm |
sort wrt. theory name;
|
changeset |
files
|
| Thu, 01 Sep 2011 16:58:03 +0200 |
wenzelm |
modernized theory name;
|
changeset |
files
|
| Thu, 01 Sep 2011 16:46:07 +0200 |
wenzelm |
repaired benchmarks;
|
changeset |
files
|
| Thu, 01 Sep 2011 14:35:51 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 01 Sep 2011 14:21:09 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 01 Sep 2011 13:18:27 +0200 |
blanchet |
always measure time for ATPs -- auto minimization relies on it
|
changeset |
files
|
| Thu, 01 Sep 2011 13:18:27 +0200 |
blanchet |
added two lemmas about "distinct" to help Sledgehammer
|
changeset |
files
|
| Thu, 01 Sep 2011 13:18:27 +0200 |
blanchet |
make "sound" sound and "unsound" more sound, based on evaluation
|
changeset |
files
|
| Thu, 01 Sep 2011 16:16:25 +0900 |
Cezary Kaliszyk |
HOL/Import: observe distinction between sets and predicates (where possible)
|
changeset |
files
|
| Wed, 31 Aug 2011 13:28:29 -0700 |
huffman |
simplify/generalize some proofs
|
changeset |
files
|
| Wed, 31 Aug 2011 10:42:31 -0700 |
huffman |
generalize lemma isCont_vec_nth
|
changeset |
files
|
| Wed, 31 Aug 2011 10:24:29 -0700 |
huffman |
convert proof to Isar-style
|
changeset |
files
|
| Wed, 31 Aug 2011 13:51:22 -0700 |
huffman |
remove redundant lemma card_enum
|
changeset |
files
|
| Wed, 31 Aug 2011 08:11:47 -0700 |
huffman |
move lemmas from Topology_Euclidean_Space to Euclidean_Space
|
changeset |
files
|
| Wed, 31 Aug 2011 07:51:55 -0700 |
huffman |
convert to Isar-style proof
|
changeset |
files
|
| Wed, 31 Aug 2011 13:22:50 +0200 |
blanchet |
make SML/NJ happy
|
changeset |
files
|
| Wed, 31 Aug 2011 11:52:03 +0200 |
blanchet |
more tuning
|
changeset |
files
|
| Wed, 31 Aug 2011 11:23:16 +0200 |
blanchet |
more tuning
|
changeset |
files
|
| Wed, 31 Aug 2011 11:14:53 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 31 Aug 2011 11:12:27 +0200 |
blanchet |
avoid relying on dubious TFF1 feature
|
changeset |
files
|
| Wed, 31 Aug 2011 08:49:10 +0200 |
blanchet |
killed FIXME (the ATP exporter outputs TPTP FOF, which is first-order)
|
changeset |
files
|
| Wed, 31 Aug 2011 08:49:10 +0200 |
blanchet |
fixed explicit declaration of TFF1 types
|
changeset |
files
|
| Tue, 30 Aug 2011 20:10:48 +0200 |
bulwahn |
adding list_size_append (thanks to Rene Thiemann)
|
changeset |
files
|
| Tue, 30 Aug 2011 20:10:47 +0200 |
bulwahn |
strengthening list_size_pointwise (thanks to Rene Thiemann)
|
changeset |
files
|
| Thu, 01 Sep 2011 14:10:52 +0200 |
wenzelm |
more flexible sorting;
|
changeset |
files
|
| Thu, 01 Sep 2011 13:39:40 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 01 Sep 2011 13:34:45 +0200 |
wenzelm |
more abstract Document.Node.Name;
|
changeset |
files
|
| Thu, 01 Sep 2011 11:33:44 +0200 |
wenzelm |
more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;
|
changeset |
files
|
| Wed, 31 Aug 2011 22:10:07 +0200 |
wenzelm |
crude display of node status;
|
changeset |
files
|
| Wed, 31 Aug 2011 20:47:33 +0200 |
wenzelm |
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
|
changeset |
files
|
| Wed, 31 Aug 2011 20:32:24 +0200 |
wenzelm |
explicit running_color;
|
changeset |
files
|
| Wed, 31 Aug 2011 19:52:13 +0200 |
wenzelm |
tuned join_commands: avoid traversing cumulative table;
|
changeset |
files
|
| Wed, 31 Aug 2011 17:36:10 +0200 |
wenzelm |
some support for theory status overview;
|
changeset |
files
|
| Wed, 31 Aug 2011 17:22:49 +0200 |
wenzelm |
tuned Commands_Changed: cover nodes as well;
|
changeset |
files
|
| Wed, 31 Aug 2011 15:41:22 +0200 |
wenzelm |
maintain name of *the* enclosing node as part of command -- avoid full document traversal;
|
changeset |
files
|
| Wed, 31 Aug 2011 14:39:41 +0200 |
wenzelm |
improved auto loading: selectable file list;
|
changeset |
files
|
| Tue, 30 Aug 2011 18:12:48 +0200 |
wenzelm |
tuned document;
|
changeset |
files
|
| Tue, 30 Aug 2011 17:53:03 +0200 |
wenzelm |
tuned import;
|
changeset |
files
|
| Tue, 30 Aug 2011 17:51:30 +0200 |
wenzelm |
tuned document;
|
changeset |
files
|
| Tue, 30 Aug 2011 17:50:41 +0200 |
wenzelm |
tuned color for Mac OS X (very light color profile?);
|
changeset |
files
|
| Tue, 30 Aug 2011 17:36:12 +0200 |
wenzelm |
tuned document;
|
changeset |
files
|
| Tue, 30 Aug 2011 17:02:06 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Tue, 30 Aug 2011 16:25:10 +0200 |
blanchet |
fixed just introduced silly bug
|
changeset |
files
|
| Tue, 30 Aug 2011 16:23:25 +0200 |
blanchet |
"simple" was renamed "mono_simple" and there's now "poly_simple" as well -- but they are not needed here since for Metis they amount to the same as guards
|
changeset |
files
|
| Tue, 30 Aug 2011 16:11:42 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:46 +0200 |
blanchet |
cleaner "pff" dummy TFF0 prover
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:46 +0200 |
blanchet |
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
added type abstractions (for declaring polymorphic constants) to TFF syntax
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
implement more of the polymorphic simply typed format TFF(1)
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
flip logic of boolean option so it's off by default
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
extended simple types with polymorphism -- the implementation still needs some work though
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
added dummy PFF prover, for debugging purposes
|
changeset |
files
|
| Tue, 30 Aug 2011 16:07:34 +0200 |
blanchet |
first step towards polymorphic TFF + changed defaults for Vampire
|
changeset |
files
|
| Tue, 30 Aug 2011 16:04:23 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 30 Aug 2011 14:29:39 +0200 |
nik |
removed explicit reliance on Hilbert_Choice.Eps
|
changeset |
files
|
| Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
improved handling of induction rules in Sledgehammer
|
changeset |
files
|
| Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
added generation of induction rules
|
changeset |
files
|
| Mon, 29 Aug 2011 13:50:47 -0700 |
huffman |
simplify some proofs
|
changeset |
files
|
| Tue, 30 Aug 2011 16:33:24 +0200 |
wenzelm |
restrict perspective to actual buffer_range, to avoid spurious edits due to faulty last_exec_offset (NB: jEdit screenlines may be silently extended by trailing newline);
|
changeset |
files
|
| Tue, 30 Aug 2011 16:04:26 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 30 Aug 2011 15:49:27 +0200 |
wenzelm |
dynamic exec state lookup for implicit position information (e.g. 'definition' without binding);
|
changeset |
files
|
| Tue, 30 Aug 2011 15:43:27 +0200 |
wenzelm |
some support for hyperlinks between different buffers;
|
changeset |
files
|
| Tue, 30 Aug 2011 12:24:55 +0200 |
wenzelm |
tuned colors -- more distance between outdated_color and quoted_color;
|
changeset |
files
|
| Tue, 30 Aug 2011 12:01:07 +0200 |
wenzelm |
do not normalized extra file dependencies for now -- still loaded by prover process;
|
changeset |
files
|
| Tue, 30 Aug 2011 11:43:47 +0200 |
wenzelm |
separate module for jEdit primitives for loading theory files;
|
changeset |
files
|
| Mon, 29 Aug 2011 22:10:08 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 29 Aug 2011 08:31:09 -0700 |
huffman |
Product_Vector.thy: clean up some proofs
|
changeset |
files
|
| Mon, 29 Aug 2011 21:55:49 +0200 |
wenzelm |
actual auto loading of required files;
|
changeset |
files
|
| Mon, 29 Aug 2011 16:38:56 +0200 |
wenzelm |
some dialog for auto loading of required files (still inactive);
|
changeset |
files
|
| Mon, 29 Aug 2011 16:28:51 +0200 |
wenzelm |
invoke in Swing thread to make double sure;
|
changeset |
files
|
| Sun, 28 Aug 2011 20:56:49 -0700 |
huffman |
move class perfect_space into RealVector.thy;
|
changeset |
files
|
| Sun, 28 Aug 2011 16:28:07 -0700 |
huffman |
generalize LIM_zero lemmas to arbitrary filters
|
changeset |
files
|
| Sun, 28 Aug 2011 09:22:42 -0700 |
huffman |
merged
|
changeset |
files
|
| Sun, 28 Aug 2011 09:20:12 -0700 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
changeset |
files
|
| Sun, 28 Aug 2011 14:16:14 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sun, 28 Aug 2011 13:13:27 +0200 |
blanchet |
split timeout among ATPs in and add Metis to the mix as backup
|
changeset |
files
|
| Sun, 28 Aug 2011 13:05:34 +0200 |
wenzelm |
more portable cp options, e.g. for non-GNU version on Mac OS X Leopard;
|
changeset |
files
|
| Sun, 28 Aug 2011 12:53:31 +0200 |
wenzelm |
tuned positions of ambiguity messages -- less intrusive in IDE view;
|
changeset |
files
|
| Sun, 28 Aug 2011 08:43:25 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sun, 28 Aug 2011 08:13:58 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sun, 28 Aug 2011 08:13:30 +0200 |
haftmann |
avoid loading List_Cset and Dlist_Cet at the same time
|
changeset |
files
|
| Sun, 28 Aug 2011 08:12:54 +0200 |
haftmann |
corrected slip
|
changeset |
files
|
| Sat, 27 Aug 2011 19:52:58 +0200 |
haftmann |
Cset, Dlist_Cset, List_Cset: restructured
|
changeset |
files
|
| Sat, 27 Aug 2011 09:44:45 +0200 |
haftmann |
Cset, Dlist_Cset, List_Cset: restructured
|
changeset |
files
|
| Sat, 27 Aug 2011 09:02:25 +0200 |
haftmann |
adapted to changes in Cset.thy
|
changeset |
files
|
| Fri, 26 Aug 2011 23:02:00 +0200 |
haftmann |
adapted to changes in Cset.thy
|
changeset |
files
|
| Fri, 26 Aug 2011 21:11:23 +0200 |
haftmann |
separating predicates and sets syntactically
|
changeset |
files
|
| Fri, 26 Aug 2011 18:24:22 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 18:23:33 +0200 |
haftmann |
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
|
changeset |
files
|
| Thu, 25 Aug 2011 23:32:12 +0200 |
haftmann |
updated generated files
|
changeset |
files
|
| Thu, 25 Aug 2011 23:20:44 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 25 Aug 2011 23:20:34 +0200 |
haftmann |
updated generated files
|
changeset |
files
|
| Sat, 27 Aug 2011 17:26:14 +0200 |
wenzelm |
explicit markup for legacy warnings;
|
changeset |
files
|
| Sat, 27 Aug 2011 16:22:59 +0200 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Sat, 27 Aug 2011 16:11:24 +0200 |
wenzelm |
less aggressive warning icon;
|
changeset |
files
|
| Sat, 27 Aug 2011 16:01:24 +0200 |
wenzelm |
tuned colors;
|
changeset |
files
|
| Sat, 27 Aug 2011 15:53:18 +0200 |
wenzelm |
transparent foreground color for quoted entities;
|
changeset |
files
|
| Sat, 27 Aug 2011 13:26:06 +0200 |
wenzelm |
more precise treatment of nodes that are fully required for partially visible ones;
|
changeset |
files
|
| Sat, 27 Aug 2011 12:22:24 +0200 |
wenzelm |
de-assigned commands also count as changed;
|
changeset |
files
|
| Sat, 27 Aug 2011 11:22:21 +0200 |
blanchet |
beef up sledgehammer_tac in Mirabelle some more
|
changeset |
files
|
| Sat, 27 Aug 2011 11:22:11 +0200 |
blanchet |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 21:52:11 +0200 |
blanchet |
change default for generation of tag idempotence and tag argument equations
|
changeset |
files
|
| Fri, 26 Aug 2011 15:11:33 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 15:11:26 -0700 |
huffman |
NEWS entry for setsum_norm ~> norm_setsum
|
changeset |
files
|
| Fri, 26 Aug 2011 15:00:00 -0700 |
huffman |
make HOL-Probability respect set/pred distinction
|
changeset |
files
|
| Fri, 26 Aug 2011 23:14:36 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 08 Sep 2010 16:10:49 -0700 |
huffman |
use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
|
changeset |
files
|
| Fri, 26 Aug 2011 10:38:29 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 08:56:29 -0700 |
huffman |
generalize and simplify proof of continuous_within_sequentially
|
changeset |
files
|
| Fri, 26 Aug 2011 08:12:38 -0700 |
huffman |
add lemma sequentially_imp_eventually_within;
|
changeset |
files
|
| Thu, 25 Aug 2011 19:41:38 -0700 |
huffman |
replace some continuous_on lemmas with more general versions
|
changeset |
files
|
| Thu, 25 Aug 2011 16:50:55 -0700 |
huffman |
remove legacy theorem Lim_inner
|
changeset |
files
|
| Thu, 25 Aug 2011 16:42:13 -0700 |
huffman |
arrange everything related to ordered_euclidean_space class together
|
changeset |
files
|
| Thu, 25 Aug 2011 16:06:50 -0700 |
huffman |
generalize and shorten proof of basis_orthogonal
|
changeset |
files
|
| Thu, 25 Aug 2011 15:35:54 -0700 |
huffman |
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
|
changeset |
files
|
| Thu, 25 Aug 2011 14:26:38 -0700 |
huffman |
merged
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:19 -0700 |
huffman |
generalize lemma finite_imp_compact_convex_hull and related lemmas
|
changeset |
files
|
| Thu, 25 Aug 2011 13:48:11 -0700 |
huffman |
generalize some lemmas
|
changeset |
files
|
| Thu, 25 Aug 2011 12:52:10 -0700 |
huffman |
generalize lemma convex_cone_hull
|
changeset |
files
|
| Thu, 25 Aug 2011 12:43:55 -0700 |
huffman |
rename subset_{interior,closure} to {interior,closure}_mono;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:57:42 -0700 |
huffman |
simplify many proofs about subspace and span;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:56:20 -0700 |
huffman |
remove duplicate simp declaration
|
changeset |
files
|
| Thu, 25 Aug 2011 09:17:02 -0700 |
huffman |
simplify definition of 'interior';
|
changeset |
files
|
| Wed, 24 Aug 2011 16:08:21 -0700 |
huffman |
add lemma closure_union;
|
changeset |
files
|
| Wed, 24 Aug 2011 15:32:40 -0700 |
huffman |
minimize imports
|
changeset |
files
|
| Wed, 24 Aug 2011 15:06:13 -0700 |
huffman |
move everything related to 'norm' method into new theory file Norm_Arith.thy
|
changeset |
files
|
| Wed, 24 Aug 2011 12:39:42 -0700 |
huffman |
remove unused lemmas dimensionI, dimension_eq
|
changeset |
files
|
| Wed, 24 Aug 2011 11:56:57 -0700 |
huffman |
move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
|
changeset |
files
|
| Fri, 26 Aug 2011 22:53:04 +0900 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| Fri, 26 Aug 2011 09:31:56 +0900 |
Cezary Kaliszyk |
FSet: Explicit proof without mem_def
|
changeset |
files
|
| Fri, 26 Aug 2011 14:54:41 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 11:22:47 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Fri, 26 Aug 2011 10:25:13 +0200 |
blanchet |
added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files
|
changeset |
files
|
| Fri, 26 Aug 2011 10:12:17 +0200 |
blanchet |
comment
|
changeset |
files
|
| Fri, 26 Aug 2011 01:18:48 +0200 |
blanchet |
disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP
|
changeset |
files
|
| Fri, 26 Aug 2011 01:14:49 +0200 |
blanchet |
improve completeness of polymorphic encodings
|
changeset |
files
|
| Fri, 26 Aug 2011 00:19:25 +0200 |
blanchet |
mangle tag bound declarations properly
|
changeset |
files
|
| Fri, 26 Aug 2011 00:05:45 +0200 |
blanchet |
fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings
|
changeset |
files
|
| Thu, 25 Aug 2011 23:55:21 +0200 |
blanchet |
make sure that if slicing is disabled, a non-SOS slice is chosen
|
changeset |
files
|
| Thu, 25 Aug 2011 23:54:57 +0200 |
blanchet |
honor TFF Implicit
|
changeset |
files
|
| Thu, 25 Aug 2011 23:38:09 +0200 |
blanchet |
make polymorphic encodings more complete
|
changeset |
files
|
| Thu, 25 Aug 2011 22:06:25 +0200 |
blanchet |
make default unsound mode less unsound
|
changeset |
files
|
| Thu, 25 Aug 2011 22:05:18 +0200 |
blanchet |
make TFF output less explicit where possible
|
changeset |
files
|
| Thu, 25 Aug 2011 19:09:39 +0200 |
blanchet |
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
|
changeset |
files
|
| Thu, 25 Aug 2011 19:05:40 +0200 |
blanchet |
added one more known Z3 failure
|
changeset |
files
|
| Thu, 25 Aug 2011 19:02:47 +0200 |
blanchet |
added config options to control two aspects of the translation, for evaluation purposes
|
changeset |
files
|
| Thu, 25 Aug 2011 13:55:52 +0100 |
nik |
added choice operator output for
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
rationalized option names -- mono becomes raw_mono and mangled becomes mono
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:06 +0200 |
blanchet |
fixed bang encoding detection of which types to encode
|
changeset |
files
|
| Thu, 25 Aug 2011 14:06:34 +0200 |
krauss |
lemma Compl_insert: "- insert x A = (-A) - {x}"
|
changeset |
files
|
| Thu, 25 Aug 2011 11:15:31 +0200 |
boehmes |
avoid variable clashes by properly incrementing indices
|
changeset |
files
|
| Thu, 25 Aug 2011 11:15:31 +0200 |
boehmes |
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
|
changeset |
files
|
| Thu, 25 Aug 2011 00:00:36 +0200 |
blanchet |
include chained facts for minimizer, otherwise it won't work
|
changeset |
files
|
| Wed, 24 Aug 2011 22:12:30 +0200 |
blanchet |
remove Vampire imconplete proof detection -- the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway
|
changeset |
files
|
| Fri, 26 Aug 2011 22:25:41 +0200 |
wenzelm |
back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;
|
changeset |
files
|
| Fri, 26 Aug 2011 22:14:12 +0200 |
wenzelm |
tuned Session.edit_node: update_perspective based on last_exec_offset;
|
changeset |
files
|
| Fri, 26 Aug 2011 21:27:58 +0200 |
wenzelm |
tuned signature -- iterate subsumes both fold and get_first;
|
changeset |
files
|
| Fri, 26 Aug 2011 21:18:42 +0200 |
wenzelm |
further clarification of Document.updated, based on last_common and after_entry;
|
changeset |
files
|
| Fri, 26 Aug 2011 16:06:58 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 26 Aug 2011 15:56:30 +0200 |
wenzelm |
improved Document.edit: more accurate update_start and no_execs;
|
changeset |
files
|
| Fri, 26 Aug 2011 15:09:54 +0200 |
wenzelm |
refined document state assignment: observe perspective, more explicit assignment message;
|
changeset |
files
|
| Thu, 25 Aug 2011 19:12:58 +0200 |
wenzelm |
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
|
changeset |
files
|
| Thu, 25 Aug 2011 17:38:12 +0200 |
wenzelm |
maintain last_execs assignment on Scala side;
|
changeset |
files
|
| Thu, 25 Aug 2011 16:44:06 +0200 |
wenzelm |
propagate information about last command with exec state assignment through document model;
|
changeset |
files
|
| Thu, 25 Aug 2011 13:24:41 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:41:48 +0200 |
wenzelm |
slightly more abstract Command.Perspective;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:27:37 +0200 |
wenzelm |
slightly more abstract Text.Perspective;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:20:05 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:19:40 +0200 |
wenzelm |
tuned syntax -- avoid ambiguities;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:00:53 +0200 |
wenzelm |
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
|
changeset |
files
|
| Wed, 24 Aug 2011 09:23:26 -0700 |
huffman |
delete commented-out dead code
|
changeset |
files
|
| Wed, 24 Aug 2011 09:08:07 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 24 Aug 2011 09:08:00 -0700 |
huffman |
change some subsection headings to subsubsection
|
changeset |
files
|
| Tue, 23 Aug 2011 16:47:48 -0700 |
huffman |
remove unnecessary lemma card_ge1
|
changeset |
files
|
| Tue, 23 Aug 2011 16:17:22 -0700 |
huffman |
move connected_real_lemma to the one place it is used
|
changeset |
files
|
| Wed, 24 Aug 2011 17:30:25 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 24 Aug 2011 15:25:39 +0200 |
blanchet |
make sure that all facts are passed to ATP from minimizer
|
changeset |
files
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
|
changeset |
files
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
specify timeout for "sledgehammer_tac"
|
changeset |
files
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 24 Aug 2011 10:59:22 +0900 |
Cezary Kaliszyk |
Quotient Package: add mem_rsp, mem_prs, tune proofs.
|
changeset |
files
|
| Tue, 23 Aug 2011 15:46:53 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 23 Aug 2011 14:11:02 -0700 |
huffman |
declare euclidean_simps [simp] at the point they are proved;
|
changeset |
files
|
| Tue, 23 Aug 2011 07:12:05 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 22 Aug 2011 18:15:33 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 22 Aug 2011 17:22:49 -0700 |
huffman |
avoid warnings
|
changeset |
files
|
| Mon, 22 Aug 2011 16:49:45 -0700 |
huffman |
comment out dead code to avoid compiler warnings
|
changeset |
files
|
| Mon, 22 Aug 2011 10:43:10 -0700 |
huffman |
legacy theorem names
|
changeset |
files
|
| Mon, 22 Aug 2011 10:19:39 -0700 |
huffman |
remove duplicate lemma
|
changeset |
files
|
| Tue, 23 Aug 2011 23:18:13 +0200 |
blanchet |
fixed "hBOOL" of existential variables, and generate more helpers
|
changeset |
files
|
| Tue, 23 Aug 2011 22:44:08 +0200 |
blanchet |
don't select facts when using sledgehammer_tac for reconstruction
|
changeset |
files
|
| Tue, 23 Aug 2011 20:35:41 +0200 |
blanchet |
don't perform a triviality check if the goal is skipped anyway
|
changeset |
files
|
| Tue, 23 Aug 2011 19:50:25 +0200 |
blanchet |
optional reconstructor
|
changeset |
files
|
| Wed, 24 Aug 2011 17:25:45 +0200 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|
| Wed, 24 Aug 2011 17:16:48 +0200 |
wenzelm |
tuned pri: prefer purging of canceled execution;
|
changeset |
files
|
| Wed, 24 Aug 2011 17:14:31 +0200 |
wenzelm |
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
|
changeset |
files
|
| Wed, 24 Aug 2011 16:49:48 +0200 |
wenzelm |
clarified Document.Node.clear -- retain header (cf. ML version);
|
changeset |
files
|
| Wed, 24 Aug 2011 16:27:27 +0200 |
wenzelm |
clarified norm_header/header_edit -- disallow update of loaded theories;
|
changeset |
files
|
| Wed, 24 Aug 2011 15:55:43 +0200 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|
| Wed, 24 Aug 2011 15:30:43 +0200 |
wenzelm |
ignore irrelevant timings;
|
changeset |
files
|
| Wed, 24 Aug 2011 13:40:10 +0200 |
wenzelm |
print state only for visible command, to avoid wasting resources for the larger part of the text;
|
changeset |
files
|
| Wed, 24 Aug 2011 13:38:07 +0200 |
wenzelm |
early filtering of unchanged perspective;
|
changeset |
files
|
| Wed, 24 Aug 2011 13:37:43 +0200 |
wenzelm |
more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
|
changeset |
files
|
| Wed, 24 Aug 2011 13:03:39 +0200 |
wenzelm |
update_perspective without actual edits, bypassing the full state assignment protocol;
|
changeset |
files
|
| Tue, 23 Aug 2011 21:19:24 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 23 Aug 2011 21:14:59 +0200 |
wenzelm |
handle potentially more approriate BufferUpdate.LOADED event;
|
changeset |
files
|
| Mon, 22 Aug 2011 23:39:05 +0200 |
wenzelm |
special treatment of structure index 1 in Pure, including legacy warning;
|
changeset |
files
|
| Tue, 23 Aug 2011 19:49:21 +0200 |
blanchet |
compile
|
changeset |
files
|
| Tue, 23 Aug 2011 19:00:48 +0200 |
blanchet |
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
|
changeset |
files
|
| Tue, 23 Aug 2011 18:42:05 +0200 |
blanchet |
beef up "sledgehammer_tac" reconstructor
|
changeset |
files
|
| Tue, 23 Aug 2011 18:42:05 +0200 |
blanchet |
clean up Sledgehammer tactic
|
changeset |
files
|
| Tue, 23 Aug 2011 17:44:31 +0200 |
wenzelm |
fixed document;
|
changeset |
files
|
| Tue, 23 Aug 2011 17:43:06 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 23 Aug 2011 17:12:54 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 23 Aug 2011 16:37:23 +0200 |
blanchet |
always use TFF if possible
|
changeset |
files
|
| Tue, 23 Aug 2011 16:14:19 +0200 |
blanchet |
clearer separator in generated file names
|
changeset |
files
|
| Tue, 23 Aug 2011 16:07:01 +0200 |
blanchet |
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
|
changeset |
files
|
| Tue, 23 Aug 2011 15:50:27 +0200 |
blanchet |
updated known failures for Z3 3.0 TPTP
|
changeset |
files
|
| Tue, 23 Aug 2011 15:18:46 +0200 |
blanchet |
updated Z3 docs
|
changeset |
files
|
| Tue, 23 Aug 2011 15:15:43 +0200 |
blanchet |
avoid TFF format with older Vampire versions
|
changeset |
files
|
| Tue, 23 Aug 2011 14:57:16 +0200 |
blanchet |
update the Vampire related parts of the documentation
|
changeset |
files
|
| Tue, 23 Aug 2011 14:44:19 +0200 |
blanchet |
fixed TFF slicing
|
changeset |
files
|
| Tue, 23 Aug 2011 14:44:19 +0200 |
blanchet |
kindly ask Vampire to output axiom names
|
changeset |
files
|
| Tue, 23 Aug 2011 14:44:19 +0200 |
blanchet |
added formats to the slice and use TFF for remote Vampire
|
changeset |
files
|
| Tue, 23 Aug 2011 07:14:09 +0200 |
haftmann |
tuned specifications, syntax and proofs
|
changeset |
files
|
| Mon, 22 Aug 2011 22:00:36 +0200 |
haftmann |
tuned specifications and syntax
|
changeset |
files
|
| Tue, 23 Aug 2011 03:34:17 +0900 |
Cezary Kaliszyk |
Quotient Package: some infrastructure for lifting inside sets
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
include all encodings in tests, now that the incompleteness of some encodings has been addressed
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
change Metis's default settings if type information axioms are generated
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
we must tag any type whose ground types intersect a nonmonotonic type
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
prefer the lighter, slightly unsound monotonicity-based encodings for Metis
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
made reconstruction of type tag equalities "\?x = \?x" reliable
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
tuning ATP problem output
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
revert guard logic -- make sure that typing information is generated for existentials
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
generate tag equations for existential variables
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
tuning, plus started implementing tag equation generation for existential variables
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
clearer terminology
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
renamed "heavy" to "uniform", based on discussion with Nick Smallbone
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
removed unused configuration option
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
added caching for (in)finiteness checks
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
remove needless typing information
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
cleaner handling of polymorphic monotonicity inference
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
more precise warning
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
added option to control soundness of encodings more precisely, for evaluation purposes
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
make sound mode more sound (and clean up code)
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
gracefully handle empty SPASS problems
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
pass sound option to Sledgehammer tactic
|
changeset |
files
|
| Tue, 23 Aug 2011 16:53:05 +0200 |
wenzelm |
tuned signature -- contrast physical output primitives versus Output.raw_message;
|
changeset |
files
|
| Tue, 23 Aug 2011 16:41:16 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 23 Aug 2011 16:39:21 +0200 |
wenzelm |
discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);
|
changeset |
files
|
| Tue, 23 Aug 2011 15:48:41 +0200 |
wenzelm |
some support for toplevel printing wrt. editor perspective (still inactive);
|
changeset |
files
|
| Tue, 23 Aug 2011 12:20:12 +0200 |
wenzelm |
propagate editor perspective through document model;
|
changeset |
files
|
| Mon, 22 Aug 2011 21:42:02 +0200 |
wenzelm |
some support for editor perspective;
|
changeset |
files
|
| Mon, 22 Aug 2011 21:09:26 +0200 |
wenzelm |
discontinued redundant Edit_Command_ID;
|
changeset |
files
|
| Mon, 22 Aug 2011 20:11:44 +0200 |
wenzelm |
reduced warnings;
|
changeset |
files
|
| Mon, 22 Aug 2011 20:00:04 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Mon, 22 Aug 2011 17:10:22 +0200 |
wenzelm |
old-style numbered structure index is legacy feature (hardly ever used now);
|
changeset |
files
|
| Mon, 22 Aug 2011 16:12:23 +0200 |
wenzelm |
added official Text.Range.Ordering;
|
changeset |
files
|
| Mon, 22 Aug 2011 14:15:52 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 22 Aug 2011 12:17:22 +0200 |
wenzelm |
reverted some odd changes to HOL/Import (cf. 74c08021ab2e);
|
changeset |
files
|
| Mon, 22 Aug 2011 10:57:33 +0200 |
krauss |
merged
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
modernized specifications
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
removed technical or trivial unused facts
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
more precise authors and comments;
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
added proof of idempotence, roughly after HOL/Subst/Unify.thy
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
tuned proofs, sledgehammering overly verbose parts
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
tuned notation
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
ported some lemmas from HOL/Subst/*;
|
changeset |
files
|
| Sun, 21 Aug 2011 22:13:04 +0200 |
krauss |
changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.
|
changeset |
files
|
| Sun, 21 Aug 2011 21:18:59 -0700 |
huffman |
merged
|
changeset |
files
|
| Sun, 21 Aug 2011 12:22:31 -0700 |
huffman |
add lemmas interior_Times and closure_Times
|
changeset |
files
|
| Sun, 21 Aug 2011 22:56:55 +0200 |
haftmann |
avoid pred/set mixture
|
changeset |
files
|
| Sun, 21 Aug 2011 19:47:52 +0200 |
haftmann |
avoid pred/set mixture
|
changeset |
files
|
| Sun, 21 Aug 2011 22:04:01 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 21 Aug 2011 11:03:15 -0700 |
huffman |
remove unnecessary euclidean_space class constraints
|
changeset |
files
|
| Sun, 21 Aug 2011 09:46:20 -0700 |
huffman |
section -> subsection
|
changeset |
files
|
| Sun, 21 Aug 2011 09:38:31 -0700 |
huffman |
scale dependency graph to fit on page
|
changeset |
files
|
| Sun, 21 Aug 2011 21:24:42 +0200 |
wenzelm |
more robust initialization of token marker and line context wrt. session startup;
|
changeset |
files
|
| Sun, 21 Aug 2011 20:42:26 +0200 |
wenzelm |
tuned Parse.group: delayed failure message;
|
changeset |
files
|
| Sun, 21 Aug 2011 20:25:49 +0200 |
wenzelm |
avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;
|
changeset |
files
|
| Sun, 21 Aug 2011 20:04:02 +0200 |
wenzelm |
default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
|
changeset |
files
|
| Sun, 21 Aug 2011 19:32:20 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 21 Aug 2011 14:16:44 +0200 |
wenzelm |
discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;
|
changeset |
files
|
| Sun, 21 Aug 2011 13:42:55 +0200 |
wenzelm |
discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;
|
changeset |
files
|
| Sun, 21 Aug 2011 13:36:23 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 20 Aug 2011 15:19:35 -0700 |
huffman |
replace lemma realpow_two_diff with new lemma square_diff_square_factored
|
changeset |
files
|
| Sat, 20 Aug 2011 15:54:26 -0700 |
huffman |
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
|
changeset |
files
|
| Sat, 20 Aug 2011 13:07:00 -0700 |
huffman |
move lemma add_eq_0_iff to Groups.thy
|
changeset |
files
|
| Sat, 20 Aug 2011 12:51:15 -0700 |
huffman |
remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead
|
changeset |
files
|
| Sat, 20 Aug 2011 10:08:47 -0700 |
huffman |
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
|
changeset |
files
|
| Sat, 20 Aug 2011 09:59:28 -0700 |
huffman |
add lemma power2_eq_iff
|
changeset |
files
|
| Sat, 20 Aug 2011 07:09:44 -0700 |
huffman |
remove some over-specific rules from the simpset
|
changeset |
files
|
| Sat, 20 Aug 2011 06:35:43 -0700 |
huffman |
merged
|
changeset |
files
|
| Sat, 20 Aug 2011 06:34:51 -0700 |
huffman |
redefine constant 'trivial_limit' as an abbreviation
|
changeset |
files
|
| Sun, 21 Aug 2011 13:23:29 +0200 |
wenzelm |
purely functional task_queue.ML -- moved actual interrupt_unsynchronized to future.ML;
|
changeset |
files
|
| Sun, 21 Aug 2011 13:10:48 +0200 |
wenzelm |
refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;
|
changeset |
files
|
| Sat, 20 Aug 2011 23:36:18 +0200 |
wenzelm |
odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
|
changeset |
files
|
| Sat, 20 Aug 2011 23:35:30 +0200 |
wenzelm |
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
|
changeset |
files
|
| Sat, 20 Aug 2011 22:46:19 +0200 |
wenzelm |
clarified get_imports -- should not rely on accidental order within graph;
|
changeset |
files
|
| Sat, 20 Aug 2011 22:28:53 +0200 |
wenzelm |
tuned Table.delete_safe: avoid potentially expensive attempt of delete;
|
changeset |
files
|
| Sat, 20 Aug 2011 20:24:12 +0200 |
wenzelm |
discontinued "Interrupt", which could disturb administrative tasks of the document model;
|
changeset |
files
|
| Sat, 20 Aug 2011 20:00:55 +0200 |
wenzelm |
more direct balanced version Ord_List.unions;
|
changeset |
files
|
| Sat, 20 Aug 2011 19:21:03 +0200 |
wenzelm |
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
|
changeset |
files
|
| Sat, 20 Aug 2011 18:11:17 +0200 |
wenzelm |
tuned future priorities (again);
|
changeset |
files
|
| Sat, 20 Aug 2011 16:06:27 +0200 |
wenzelm |
clarified fulfill_norm_proof: no join_thms yet;
|
changeset |
files
|
| Sat, 20 Aug 2011 15:52:29 +0200 |
wenzelm |
added Future.joins convenience;
|
changeset |
files
|
| Sat, 20 Aug 2011 09:42:34 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sat, 20 Aug 2011 09:42:12 +0200 |
haftmann |
deactivated »unknown« nitpick example
|
changeset |
files
|
| Sat, 20 Aug 2011 09:30:23 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sat, 20 Aug 2011 01:40:22 +0200 |
haftmann |
tuned proof
|
changeset |
files
|
| Sat, 20 Aug 2011 01:39:27 +0200 |
haftmann |
more uniform formatting of specifications
|
changeset |
files
|
| Sat, 20 Aug 2011 01:33:58 +0200 |
haftmann |
compatibility layer
|
changeset |
files
|
| Sat, 20 Aug 2011 01:21:22 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 19 Aug 2011 19:33:31 +0200 |
haftmann |
more concise definition for Inf, Sup on bool
|
changeset |
files
|
| Thu, 18 Aug 2011 13:37:41 +0200 |
noschinl |
do not call ghc with -fglasgow-exts
|
changeset |
files
|
| Fri, 19 Aug 2011 19:01:00 -0700 |
huffman |
remove some redundant simp rules about sqrt
|
changeset |
files
|
| Fri, 19 Aug 2011 18:42:41 -0700 |
huffman |
move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
|
changeset |
files
|
| Fri, 19 Aug 2011 18:08:05 -0700 |
huffman |
remove unused lemma DERIV_sin_add
|
changeset |
files
|
| Fri, 19 Aug 2011 18:06:27 -0700 |
huffman |
remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
|
changeset |
files
|
| Fri, 19 Aug 2011 17:59:19 -0700 |
huffman |
remove redundant lemma exp_ln_eq in favor of ln_unique
|
changeset |
files
|
| Fri, 19 Aug 2011 16:55:43 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 19 Aug 2011 15:54:43 -0700 |
huffman |
Lim.thy: legacy theorems
|
changeset |
files
|
| Fri, 19 Aug 2011 15:07:10 -0700 |
huffman |
SEQ.thy: legacy theorem names
|
changeset |
files
|
| Fri, 19 Aug 2011 14:46:45 -0700 |
huffman |
delete unused lemmas about limits
|
changeset |
files
|
| Fri, 19 Aug 2011 14:17:28 -0700 |
huffman |
Transcendental.thy: add tendsto_intros lemmas;
|
changeset |
files
|
| Fri, 19 Aug 2011 11:49:53 -0700 |
huffman |
add lemma isCont_tendsto_compose
|
changeset |
files
|
| Fri, 19 Aug 2011 23:48:18 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 19 Aug 2011 10:46:54 -0700 |
huffman |
Transcendental.thy: remove several unused lemmas and simplify some proofs
|
changeset |
files
|
| Fri, 19 Aug 2011 08:40:15 -0700 |
huffman |
remove unused lemmas
|
changeset |
files
|
| Fri, 19 Aug 2011 08:39:43 -0700 |
huffman |
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
|
changeset |
files
|
| Fri, 19 Aug 2011 07:45:22 -0700 |
huffman |
remove some redundant simp rules
|
changeset |
files
|
| Fri, 19 Aug 2011 23:25:47 +0200 |
wenzelm |
maintain recent future proofs at transaction boundaries;
|
changeset |
files
|
| Fri, 19 Aug 2011 21:40:52 +0200 |
wenzelm |
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;
|
changeset |
files
|
| Fri, 19 Aug 2011 18:01:23 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 19 Aug 2011 17:39:37 +0200 |
wenzelm |
tuned signature (again);
|
changeset |
files
|
| Fri, 19 Aug 2011 16:13:26 +0200 |
wenzelm |
tuned signature -- treat structure Task_Queue as private to implementation;
|
changeset |
files
|
| Fri, 19 Aug 2011 15:56:26 +0200 |
wenzelm |
refined Future.cancel: explicit future allows to join actual cancellation;
|
changeset |
files
|
| Fri, 19 Aug 2011 14:01:20 +0200 |
wenzelm |
Future.promise: explicit abort operation (like uninterruptible future job);
|
changeset |
files
|
| Fri, 19 Aug 2011 13:55:32 +0200 |
wenzelm |
editable raw text areas: allow user to clear content;
|
changeset |
files
|
| Fri, 19 Aug 2011 13:32:27 +0200 |
wenzelm |
more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
|
changeset |
files
|
| Fri, 19 Aug 2011 12:51:14 +0200 |
wenzelm |
more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
|
changeset |
files
|
| Fri, 19 Aug 2011 12:03:44 +0200 |
wenzelm |
clarified Future.cond_forks: more uniform handling of exceptional situations;
|
changeset |
files
|
| Fri, 19 Aug 2011 17:05:10 +0900 |
Cezary Kaliszyk |
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
|
changeset |
files
|
| Thu, 18 Aug 2011 22:32:19 -0700 |
huffman |
merged
|
changeset |
files
|
| Thu, 18 Aug 2011 22:31:52 -0700 |
huffman |
define complex exponential 'expi' as abbreviation for 'exp'
|
changeset |
files
|
| Thu, 18 Aug 2011 21:23:31 -0700 |
huffman |
remove more bounded_linear locale interpretations (cf. f0de18b62d63)
|
changeset |
files
|
| Thu, 18 Aug 2011 19:53:03 -0700 |
huffman |
optimize some proofs
|
changeset |
files
|
| Thu, 18 Aug 2011 18:10:23 -0700 |
huffman |
add Multivariate_Analysis dependencies
|
changeset |
files
|
| Thu, 18 Aug 2011 18:08:43 -0700 |
huffman |
import Library/Sum_of_Squares instead of reloading positivstellensatz.ML
|
changeset |
files
|
| Thu, 18 Aug 2011 17:32:02 -0700 |
huffman |
declare euclidean_component_zero[simp] at the point it is proved
|
changeset |
files
|
| Fri, 19 Aug 2011 10:23:16 +0900 |
Cezary Kaliszyk |
Quotient Package: Regularization: do not fail if no progress is made, leave the subgoal to the user. Injection: try assumptions before extensionality to avoid looping.
|
changeset |
files
|
| Thu, 18 Aug 2011 23:43:22 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Thu, 18 Aug 2011 14:08:39 -0700 |
huffman |
merged
|
changeset |
files
|
| Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
changeset |
files
|
| Thu, 18 Aug 2011 22:50:28 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 18 Aug 2011 22:50:17 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 18 Aug 2011 14:01:06 +0200 |
haftmann |
avoid duplicated simp add option
|
changeset |
files
|
| Thu, 18 Aug 2011 13:55:26 +0200 |
haftmann |
observe distinction between sets and predicates more properly
|
changeset |
files
|
| Thu, 18 Aug 2011 13:25:17 +0200 |
haftmann |
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
|
changeset |
files
|
| Thu, 18 Aug 2011 13:10:24 +0200 |
haftmann |
avoid case-sensitive name for example theory
|
changeset |
files
|
| Thu, 18 Aug 2011 17:42:35 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 18 Aug 2011 17:42:18 +0200 |
nipkow |
case_names NEWS
|
changeset |
files
|
| Thu, 18 Aug 2011 17:00:15 +0200 |
bulwahn |
adding documentation about simps equation in the inductive package
|
changeset |
files
|
| Thu, 18 Aug 2011 12:06:17 +0200 |
bulwahn |
activating narrowing-based quickcheck by default
|
changeset |
files
|
| Thu, 18 Aug 2011 18:07:40 +0200 |
wenzelm |
more precise treatment of exception nesting and serial numbers;
|
changeset |
files
|
| Thu, 18 Aug 2011 17:53:32 +0200 |
wenzelm |
more careful treatment of exception serial numbers, with propagation to message channel;
|
changeset |
files
|
| Thu, 18 Aug 2011 17:30:47 +0200 |
wenzelm |
updated sequential version (cf. b94951f06e48);
|
changeset |
files
|
| Thu, 18 Aug 2011 16:07:58 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Thu, 18 Aug 2011 15:51:34 +0200 |
wenzelm |
tuned document;
|
changeset |
files
|
| Thu, 18 Aug 2011 15:39:00 +0200 |
wenzelm |
clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;
|
changeset |
files
|
| Thu, 18 Aug 2011 15:37:01 +0200 |
wenzelm |
export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;
|
changeset |
files
|
| Thu, 18 Aug 2011 15:15:43 +0200 |
wenzelm |
tune Par_Exn.make: balance merge;
|
changeset |
files
|
| Thu, 18 Aug 2011 16:52:19 +0900 |
Cezary Kaliszyk |
Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.
|
changeset |
files
|
| Wed, 17 Aug 2011 15:12:34 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 17 Aug 2011 15:03:30 -0700 |
huffman |
HOL-IMP: respect set/pred distinction
|
changeset |
files
|
| Wed, 17 Aug 2011 15:02:17 -0700 |
huffman |
Determinants.thy: avoid using mem_def/Collect_def
|
changeset |
files
|
| Wed, 17 Aug 2011 14:42:59 -0700 |
huffman |
Wfrec.thy: respect set/pred distinction
|
changeset |
files
|
| Thu, 18 Aug 2011 00:02:44 +0200 |
wenzelm |
follow updates of Isabelle/Pure;
|
changeset |
files
|
| Wed, 17 Aug 2011 23:41:47 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 17 Aug 2011 14:32:48 -0700 |
huffman |
IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library
|
changeset |
files
|
| Wed, 17 Aug 2011 13:10:49 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 17 Aug 2011 13:10:11 -0700 |
huffman |
Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems
|
changeset |
files
|
| Wed, 17 Aug 2011 11:39:09 -0700 |
huffman |
add lemma tendsto_compose_eventually; use it to shorten some proofs
|
changeset |
files
|
| Wed, 17 Aug 2011 11:07:32 -0700 |
huffman |
Topology_Euclidean_Space.thy: simplify some proofs
|
changeset |
files
|
| Wed, 17 Aug 2011 11:06:39 -0700 |
huffman |
add lemma metric_tendsto_imp_tendsto
|
changeset |
files
|
| Wed, 17 Aug 2011 09:59:10 -0700 |
huffman |
simplify proofs of lemmas open_interval, closed_interval
|
changeset |
files
|
| Wed, 17 Aug 2011 23:37:23 +0200 |
wenzelm |
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
|
changeset |
files
|
| Wed, 17 Aug 2011 22:25:00 +0200 |
wenzelm |
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
|
changeset |
files
|
| Wed, 17 Aug 2011 22:14:22 +0200 |
wenzelm |
more systematic handling of parallel exceptions;
|
changeset |
files
|
| Wed, 17 Aug 2011 20:08:36 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 17 Aug 2011 18:52:21 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 17 Aug 2011 18:51:27 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 17 Aug 2011 07:13:13 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 16 Aug 2011 19:47:50 +0200 |
haftmann |
avoid Collect_def in proof
|
changeset |
files
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
changeset |
files
|
| Wed, 17 Aug 2011 16:46:58 +0200 |
wenzelm |
improved default context for ML toplevel pretty-printing;
|
changeset |
files
|
| Wed, 17 Aug 2011 16:30:38 +0200 |
wenzelm |
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
|
changeset |
files
|
| Wed, 17 Aug 2011 16:01:27 +0200 |
wenzelm |
some convenience actions/shortcuts for control symbols;
|
changeset |
files
|
| Wed, 17 Aug 2011 15:14:48 +0200 |
wenzelm |
export Function_Fun.fun_config for user convenience;
|
changeset |
files
|
| Wed, 17 Aug 2011 13:14:20 +0200 |
wenzelm |
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
|
changeset |
files
|
| Wed, 17 Aug 2011 10:03:58 +0200 |
blanchet |
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
|
changeset |
files
|
| Tue, 16 Aug 2011 15:02:20 -0700 |
huffman |
merged
|
changeset |
files
|
| Tue, 16 Aug 2011 09:31:23 -0700 |
huffman |
add simp rules for isCont
|
changeset |
files
|
| Tue, 16 Aug 2011 23:39:58 +0200 |
wenzelm |
updated keywords -- old codegen is no longer in Pure;
|
changeset |
files
|
| Tue, 16 Aug 2011 23:39:30 +0200 |
wenzelm |
include HOL-Library keywords for the sake of recdef;
|
changeset |
files
|
| Tue, 16 Aug 2011 23:25:02 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 16 Aug 2011 13:07:52 -0700 |
huffman |
Multivariate_Analysis includes Determinants.thy, but doesn't import it by default
|
changeset |
files
|
| Tue, 16 Aug 2011 07:56:17 -0700 |
huffman |
get Multivariate_Analysis/Determinants.thy compiled and working again
|
changeset |
files
|
| Tue, 16 Aug 2011 07:06:54 -0700 |
huffman |
get Library/Permutations.thy compiled and working again
|
changeset |
files
|
| Tue, 16 Aug 2011 23:17:26 +0200 |
wenzelm |
workaround for Cygwin, to make it work in the important special case without extra files;
|
changeset |
files
|
| Tue, 16 Aug 2011 22:48:31 +0200 |
wenzelm |
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
|
changeset |
files
|
| Tue, 16 Aug 2011 21:54:06 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Tue, 16 Aug 2011 21:50:53 +0200 |
wenzelm |
more robust treatment of node dependencies in incremental edits;
|
changeset |
files
|
| Tue, 16 Aug 2011 21:13:52 +0200 |
wenzelm |
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
|
changeset |
files
|
| Tue, 16 Aug 2011 12:06:49 +0200 |
wenzelm |
omit MiscUtilities.resolveSymlinks for now -- odd effects on case-insensible file-system;
|
changeset |
files
|
| Mon, 15 Aug 2011 19:42:52 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 15 Aug 2011 18:35:36 -0700 |
huffman |
generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space
|
changeset |
files
|
| Mon, 15 Aug 2011 16:48:05 -0700 |
huffman |
add lemma tendsto_compose
|
changeset |
files
|
| Mon, 15 Aug 2011 16:18:13 -0700 |
huffman |
remove extraneous subsection heading
|
changeset |
files
|
| Mon, 15 Aug 2011 15:11:55 -0700 |
huffman |
generalized lemma closed_Collect_eq
|
changeset |
files
|
| Mon, 15 Aug 2011 14:50:24 -0700 |
huffman |
remove duplicate lemma disjoint_iff
|
changeset |
files
|
| Mon, 15 Aug 2011 14:29:17 -0700 |
huffman |
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
|
changeset |
files
|
| Mon, 15 Aug 2011 14:09:39 -0700 |
huffman |
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
|
changeset |
files
|
| Mon, 15 Aug 2011 12:18:34 -0700 |
huffman |
generalize lemma continuous_uniform_limit to class metric_space
|
changeset |
files
|
| Mon, 15 Aug 2011 12:13:46 -0700 |
huffman |
remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
|
changeset |
files
|
| Mon, 15 Aug 2011 10:49:48 -0700 |
huffman |
Topology_Euclidean_Space.thy: organize section headings
|
changeset |
files
|
| Mon, 15 Aug 2011 09:08:17 -0700 |
huffman |
simplify some proofs
|
changeset |
files
|
| Sun, 14 Aug 2011 13:04:57 -0700 |
huffman |
generalize lemma convergent_subseq_convergent
|
changeset |
files
|
| Sun, 14 Aug 2011 11:44:12 -0700 |
huffman |
locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
|
changeset |
files
|
| Sun, 14 Aug 2011 10:47:47 -0700 |
huffman |
locale-ize some constant definitions, so complete_space can inherit from metric_space
|
changeset |
files
|
| Sun, 14 Aug 2011 10:25:43 -0700 |
huffman |
generalize constant 'lim' and limit uniqueness theorems to class t2_space
|
changeset |
files
|
| Tue, 16 Aug 2011 07:17:15 +0900 |
Cezary Kaliszyk |
Quotient Package: make quotient_type work with separate set type
|
changeset |
files
|
| Mon, 15 Aug 2011 22:31:17 +0200 |
wenzelm |
updated README;
|
changeset |
files
|
| Mon, 15 Aug 2011 21:54:32 +0200 |
wenzelm |
touch descendants of edited nodes;
|
changeset |
files
|
| Mon, 15 Aug 2011 21:05:30 +0200 |
wenzelm |
parellel scheduling of node edits and execution;
|
changeset |
files
|
| Mon, 15 Aug 2011 20:38:16 +0200 |
wenzelm |
tuned error message;
|
changeset |
files
|
| Mon, 15 Aug 2011 20:19:41 +0200 |
wenzelm |
retrieve imports from document state, with fall-back on theory loader for preloaded theories;
|
changeset |
files
|
| Mon, 15 Aug 2011 19:27:55 +0200 |
wenzelm |
explicit check of finished evaluation;
|
changeset |
files
|
| Mon, 15 Aug 2011 16:38:42 +0200 |
wenzelm |
refined Document.edit: less stateful update via Graph.schedule;
|
changeset |
files
|
| Mon, 15 Aug 2011 14:54:36 +0200 |
wenzelm |
simplified exec: eliminated unused status flag;
|
changeset |
files
|
| Sun, 14 Aug 2011 08:45:38 -0700 |
huffman |
consistently use variable name 'F' for filters
|
changeset |
files
|
| Sun, 14 Aug 2011 07:54:24 -0700 |
huffman |
generalize lemmas about LIM and LIMSEQ to tendsto
|
changeset |
files
|
| Sat, 13 Aug 2011 18:10:14 -0700 |
huffman |
HOL-Nominal-Examples: respect distinction between sets and functions
|
changeset |
files
|
| Sat, 13 Aug 2011 22:04:07 +0200 |
wenzelm |
less verbosity in batch mode -- spam reduction and notable performance improvement;
|
changeset |
files
|
| Sat, 13 Aug 2011 21:28:01 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 13 Aug 2011 07:56:55 -0700 |
huffman |
HOL-Hahn_Banach: use Set_Algebras library
|
changeset |
files
|
| Sat, 13 Aug 2011 07:39:35 -0700 |
huffman |
ex/Quickcheck_Examples.thy: respect distinction between sets and functions
|
changeset |
files
|
| Sat, 13 Aug 2011 21:06:01 +0200 |
wenzelm |
clarified Toplevel.end_theory;
|
changeset |
files
|
| Sat, 13 Aug 2011 20:49:41 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special name argument;
|
changeset |
files
|
| Sat, 13 Aug 2011 20:41:29 +0200 |
wenzelm |
simplified Toplevel.init_theory: discontinued special master argument;
|
changeset |
files
|
| Sat, 13 Aug 2011 20:20:36 +0200 |
wenzelm |
provide node header via Scala layer;
|
changeset |
files
|
| Sat, 13 Aug 2011 16:07:26 +0200 |
wenzelm |
reduced verbosity;
|
changeset |
files
|
| Sat, 13 Aug 2011 16:04:28 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 13 Aug 2011 15:59:26 +0200 |
wenzelm |
clarified node header -- exclude master_dir;
|
changeset |
files
|
| Sat, 13 Aug 2011 13:48:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 13 Aug 2011 13:42:35 +0200 |
wenzelm |
maintain node header;
|
changeset |
files
|
| Sat, 13 Aug 2011 12:23:51 +0200 |
kleing |
removed unused lemma; removed old-style ;
|
changeset |
files
|
| Sat, 13 Aug 2011 12:05:52 +0200 |
kleing |
point isatest-statistics to the right afp log files
|
changeset |
files
|
| Sat, 13 Aug 2011 11:57:13 +0200 |
kleing |
IMP/Util distinguishes between sets and functions again; imported only where used.
|
changeset |
files
|
| Fri, 12 Aug 2011 20:55:22 -0700 |
huffman |
remove redundant lemma setsum_norm in favor of norm_setsum;
|
changeset |
files
|
| Fri, 12 Aug 2011 16:47:53 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 12 Aug 2011 14:45:50 -0700 |
huffman |
make more HOL theories work with separate set type
|
changeset |
files
|
| Sat, 13 Aug 2011 00:34:54 +0200 |
wenzelm |
immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
|
changeset |
files
|
| Fri, 12 Aug 2011 23:29:28 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 12 Aug 2011 09:17:30 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 12 Aug 2011 09:17:24 -0700 |
huffman |
make Multivariate_Analysis work with separate set type
|
changeset |
files
|
| Fri, 12 Aug 2011 07:18:28 -0700 |
huffman |
make HOLCF work with separate set type
|
changeset |
files
|
| Fri, 12 Aug 2011 07:13:12 -0700 |
huffman |
merged
|
changeset |
files
|
| Thu, 11 Aug 2011 14:24:05 -0700 |
huffman |
avoid duplicate rule warnings
|
changeset |
files
|
| Thu, 11 Aug 2011 13:05:56 -0700 |
huffman |
modify euclidean_space class to include basis set
|
changeset |
files
|
| Thu, 11 Aug 2011 09:11:15 -0700 |
huffman |
remove lemma stupid_ext
|
changeset |
files
|
| Fri, 12 Aug 2011 17:01:30 +0200 |
nipkow |
documented extended version of case_names attribute
|
changeset |
files
|
| Fri, 12 Aug 2011 22:10:49 +0200 |
wenzelm |
normalized theory dependencies wrt. file_store;
|
changeset |
files
|
| Fri, 12 Aug 2011 20:32:25 +0200 |
wenzelm |
general Graph.schedule;
|
changeset |
files
|
| Fri, 12 Aug 2011 15:30:12 +0200 |
wenzelm |
allow "$" within basic path elements (NB: initial "$" refers to path variable);
|
changeset |
files
|
| Fri, 12 Aug 2011 15:28:30 +0200 |
wenzelm |
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
|
changeset |
files
|
| Fri, 12 Aug 2011 12:03:17 +0200 |
wenzelm |
simplified class Thy_Header;
|
changeset |
files
|
| Fri, 12 Aug 2011 11:41:26 +0200 |
wenzelm |
clarified Exn.message;
|
changeset |
files
|
| Thu, 11 Aug 2011 20:32:44 +0200 |
wenzelm |
uniform treatment of header edits as document edits;
|
changeset |
files
|
| Thu, 11 Aug 2011 18:01:28 +0200 |
wenzelm |
explicit datatypes for document node edits;
|
changeset |
files
|
| Thu, 11 Aug 2011 13:24:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Aug 2011 13:22:22 +0200 |
wenzelm |
disentangled nested ML files;
|
changeset |
files
|
| Thu, 11 Aug 2011 13:05:23 +0200 |
wenzelm |
minimal script to run raw Poly/ML with concurrency library;
|
changeset |
files
|
| Thu, 11 Aug 2011 12:53:41 +0200 |
wenzelm |
somewhat more uniform THIS;
|
changeset |
files
|
| Thu, 11 Aug 2011 12:49:14 +0200 |
wenzelm |
more trimming;
|
changeset |
files
|
| Thu, 11 Aug 2011 12:30:41 +0200 |
wenzelm |
recovered some ML toplevel pp;
|
changeset |
files
|
| Thu, 11 Aug 2011 12:24:10 +0200 |
wenzelm |
some trimming;
|
changeset |
files
|
| Thu, 11 Aug 2011 12:11:50 +0200 |
wenzelm |
prefix of Pure/ROOT.ML required for concurrency within the ML runtime;
|
changeset |
files
|
| Thu, 11 Aug 2011 11:40:25 +0200 |
wenzelm |
redundant use of misc_legacy.ML;
|
changeset |
files
|
| Thu, 11 Aug 2011 10:36:34 +0200 |
krauss |
eliminated use of recdef
|
changeset |
files
|
| Thu, 11 Aug 2011 09:41:21 +0200 |
krauss |
removed obsolete recdef-related examples
|
changeset |
files
|
| Thu, 11 Aug 2011 09:15:45 +0200 |
krauss |
removed unused material, which does not really belong here
|
changeset |
files
|
| Wed, 10 Aug 2011 18:07:32 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 10 Aug 2011 18:02:16 -0700 |
huffman |
avoid warnings about duplicate rules
|
changeset |
files
|
| Wed, 10 Aug 2011 17:02:03 -0700 |
huffman |
follow standard naming scheme for sgn_vec_def
|
changeset |
files
|
| Wed, 10 Aug 2011 16:35:50 -0700 |
huffman |
remove several redundant and unused theorems about derivatives
|
changeset |
files
|
| Wed, 10 Aug 2011 15:56:48 -0700 |
huffman |
remove redundant lemma
|
changeset |
files
|
| Wed, 10 Aug 2011 14:25:56 -0700 |
huffman |
simplify proof of lemma bounded_component
|
changeset |
files
|
| Wed, 10 Aug 2011 14:10:52 -0700 |
huffman |
simplify some proofs
|
changeset |
files
|
| Wed, 10 Aug 2011 13:13:37 -0700 |
huffman |
more uniform naming scheme for finite cartesian product type and related theorems
|
changeset |
files
|
| Wed, 10 Aug 2011 10:13:16 -0700 |
huffman |
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
|
changeset |
files
|
| Wed, 10 Aug 2011 21:24:26 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 10 Aug 2011 09:23:42 -0700 |
huffman |
split Linear_Algebra.thy from Euclidean_Space.thy
|
changeset |
files
|
| Wed, 10 Aug 2011 08:42:26 -0700 |
huffman |
full import paths
|
changeset |
files
|
| Wed, 10 Aug 2011 01:36:53 -0700 |
huffman |
declare tendsto_const [intro] (accidentally removed in 230a8665c919)
|
changeset |
files
|
| Wed, 10 Aug 2011 00:31:51 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 10 Aug 2011 00:29:31 -0700 |
huffman |
simplified definition of class euclidean_space;
|
changeset |
files
|
| Tue, 09 Aug 2011 13:09:35 -0700 |
huffman |
bounded_linear interpretation for euclidean_component
|
changeset |
files
|
| Tue, 09 Aug 2011 12:50:22 -0700 |
huffman |
lemma bounded_linear_intro
|
changeset |
files
|
| Tue, 09 Aug 2011 10:42:07 -0700 |
huffman |
avoid duplicate rewrite warnings
|
changeset |
files
|
| Tue, 09 Aug 2011 10:30:00 -0700 |
huffman |
mark some redundant theorems as legacy
|
changeset |
files
|
| Tue, 09 Aug 2011 08:53:12 -0700 |
huffman |
Derivative.thy: more sensible subsection headings
|
changeset |
files
|
| Tue, 09 Aug 2011 07:37:18 -0700 |
huffman |
Derivative.thy: clean up formatting
|
changeset |
files
|
| Mon, 08 Aug 2011 21:17:52 -0700 |
huffman |
instance real_basis_with_inner < perfect_space
|
changeset |
files
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
changeset |
files
|
| Wed, 10 Aug 2011 20:12:36 +0200 |
wenzelm |
moved old code generator to src/Tools/;
|
changeset |
files
|
| Wed, 10 Aug 2011 19:46:48 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
changeset |
files
|
| Wed, 10 Aug 2011 19:45:57 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
changeset |
files
|
| Wed, 10 Aug 2011 19:45:41 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
changeset |
files
|
| Wed, 10 Aug 2011 19:21:28 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
changeset |
files
|
| Wed, 10 Aug 2011 16:26:05 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 10 Aug 2011 16:24:39 +0200 |
wenzelm |
Goal.forked: clarified handling of interrupts;
|
changeset |
files
|
| Wed, 10 Aug 2011 16:05:14 +0200 |
wenzelm |
future_job: explicit indication of interrupts;
|
changeset |
files
|
| Wed, 10 Aug 2011 15:17:24 +0200 |
wenzelm |
more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;
|
changeset |
files
|
| Wed, 10 Aug 2011 14:28:55 +0200 |
wenzelm |
synchronized cancel and flushing of Multithreading.interrupted state, to ensure that interrupts stay within task boundaries;
|
changeset |
files
|
| Wed, 10 Aug 2011 14:04:45 +0200 |
wenzelm |
tuned source structure;
|
changeset |
files
|
| Wed, 10 Aug 2011 10:59:37 +0200 |
wenzelm |
bash_output_fifo blocks on Cygwin 1.7.x;
|
changeset |
files
|
| Tue, 09 Aug 2011 23:54:17 +0200 |
berghofe |
rename_bvs now avoids introducing name clashes between schematic variables
|
changeset |
files
|
| Tue, 09 Aug 2011 22:37:33 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 09 Aug 2011 20:24:48 +0200 |
haftmann |
tuned proofs
|
changeset |
files
|
| Tue, 09 Aug 2011 18:52:18 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 09 Aug 2011 08:07:22 +0200 |
haftmann |
tuned header
|
changeset |
files
|
| Tue, 09 Aug 2011 08:06:15 +0200 |
haftmann |
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
|
changeset |
files
|
| Tue, 09 Aug 2011 16:09:10 +0200 |
kleing |
removed "extremely ambigous" warning; has been ignored by everyone for years.
|
changeset |
files
|
| Tue, 09 Aug 2011 22:30:33 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Tue, 09 Aug 2011 21:48:36 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Tue, 09 Aug 2011 17:33:17 +0200 |
blanchet |
support local HOATPs
|
changeset |
files
|
| Tue, 09 Aug 2011 17:33:17 +0200 |
blanchet |
document local HOATPs
|
changeset |
files
|
| Tue, 09 Aug 2011 17:33:17 +0200 |
blanchet |
workaround THF parser limitation
|
changeset |
files
|
| Tue, 09 Aug 2011 17:33:17 +0200 |
blanchet |
LEO-II also supports FOF
|
changeset |
files
|
| Tue, 09 Aug 2011 15:50:13 +0200 |
wenzelm |
misc tuning and simplification;
|
changeset |
files
|
| Tue, 09 Aug 2011 15:41:00 +0200 |
wenzelm |
updated documentation of method "split" according to e6a4bb832b46;
|
changeset |
files
|
| Tue, 09 Aug 2011 09:39:49 +0200 |
blanchet |
updated references to CADE-23
|
changeset |
files
|
| Tue, 09 Aug 2011 09:33:50 +0200 |
blanchet |
renamed E wrappers for consistency with CASC conventions
|
changeset |
files
|
| Tue, 09 Aug 2011 09:33:01 +0200 |
blanchet |
updated Sledgehammer docs
|
changeset |
files
|
| Tue, 09 Aug 2011 09:24:34 +0200 |
blanchet |
add line number prefix to output file name
|
changeset |
files
|
| Tue, 09 Aug 2011 09:07:59 +0200 |
blanchet |
added "sound" option to Mirabelle
|
changeset |
files
|
| Tue, 09 Aug 2011 09:05:22 +0200 |
blanchet |
move lambda-lifting code to ATP encoding, so it can be used by Metis
|
changeset |
files
|
| Tue, 09 Aug 2011 09:05:21 +0200 |
blanchet |
load lambda-lifting structure earlier, so it can be used in Metis
|
changeset |
files
|
| Tue, 09 Aug 2011 07:44:17 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 08 Aug 2011 22:33:36 +0200 |
haftmann |
move legacy candiates to bottom; marked candidates for default simp rules
|
changeset |
files
|
| Mon, 08 Aug 2011 22:11:00 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 08 Aug 2011 19:30:18 +0200 |
haftmann |
dropped lemmas (Inf|Sup)_(singleton|binary)
|
changeset |
files
|
| Mon, 08 Aug 2011 19:21:11 +0200 |
haftmann |
dropped lemmas (Inf|Sup)_(singleton|binary)
|
changeset |
files
|
| Mon, 08 Aug 2011 19:26:53 -0700 |
huffman |
rename type 'a net to 'a filter, following standard mathematical terminology
|
changeset |
files
|
| Mon, 08 Aug 2011 18:36:32 -0700 |
huffman |
HOLCF: fix warnings about unreferenced identifiers
|
changeset |
files
|
| Mon, 08 Aug 2011 16:57:37 -0700 |
huffman |
remove duplicate lemmas
|
changeset |
files
|
| Mon, 08 Aug 2011 16:19:57 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 08 Aug 2011 16:04:58 -0700 |
huffman |
fix perfect_space instance proof for finite cartesian product (cf. 5b970711fb39)
|
changeset |
files
|
| Mon, 08 Aug 2011 15:27:24 -0700 |
huffman |
generalize sequence lemmas
|
changeset |
files
|
| Mon, 08 Aug 2011 15:11:38 -0700 |
huffman |
generalize more lemmas about compactness
|
changeset |
files
|
| Mon, 08 Aug 2011 15:03:34 -0700 |
huffman |
generalize compactness equivalence lemmas
|
changeset |
files
|
| Mon, 08 Aug 2011 14:59:01 -0700 |
huffman |
lemma bolzano_weierstrass_imp_compact
|
changeset |
files
|
| Mon, 08 Aug 2011 14:44:20 -0700 |
huffman |
class perfect_space inherits from topological_space;
|
changeset |
files
|
| Mon, 08 Aug 2011 21:55:01 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 08 Aug 2011 16:47:55 +0200 |
kleing |
import constant folding theory into IMP
|
changeset |
files
|
| Sat, 06 Aug 2011 15:48:08 +0200 |
kleing |
make syntax ambiguity warnings a config option
|
changeset |
files
|
| Mon, 08 Aug 2011 11:47:41 -0700 |
huffman |
add lemmas INF_image, SUP_image
|
changeset |
files
|
| Mon, 08 Aug 2011 11:25:18 -0700 |
huffman |
declare {INF,SUP}_empty [simp]
|
changeset |
files
|
| Mon, 08 Aug 2011 10:32:55 -0700 |
huffman |
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
|
changeset |
files
|
| Mon, 08 Aug 2011 10:26:26 -0700 |
huffman |
standard theorem naming scheme: complex_eqI, complex_eq_iff
|
changeset |
files
|
| Mon, 08 Aug 2011 09:52:09 -0700 |
huffman |
moved division ring stuff from Rings.thy to Fields.thy
|
changeset |
files
|
| Mon, 08 Aug 2011 08:55:49 -0700 |
huffman |
Library/Product_ord: wellorder instance for products
|
changeset |
files
|
| Mon, 08 Aug 2011 21:11:10 +0200 |
wenzelm |
modernized file proof_checker.ML;
|
changeset |
files
|
| Mon, 08 Aug 2011 20:47:12 +0200 |
wenzelm |
tuned thm_of_proof: build lookup table within closure;
|
changeset |
files
|
| Mon, 08 Aug 2011 20:21:49 +0200 |
wenzelm |
added Reconstruct.proof_of convenience;
|
changeset |
files
|
| Mon, 08 Aug 2011 19:59:35 +0200 |
wenzelm |
ship message in one piece;
|
changeset |
files
|
| Mon, 08 Aug 2011 17:23:15 +0200 |
wenzelm |
misc tuning -- eliminated old-fashioned rep_thm;
|
changeset |
files
|
| Mon, 08 Aug 2011 16:38:59 +0200 |
wenzelm |
modernized strcture Proof_Checker;
|
changeset |
files
|
| Mon, 08 Aug 2011 16:09:34 +0200 |
wenzelm |
less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
|
changeset |
files
|
| Mon, 08 Aug 2011 13:48:38 +0200 |
wenzelm |
updated imports;
|
changeset |
files
|
| Mon, 08 Aug 2011 13:40:24 +0200 |
wenzelm |
proper signature;
|
changeset |
files
|
| Mon, 08 Aug 2011 13:39:51 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Mon, 08 Aug 2011 13:29:54 +0200 |
wenzelm |
slightly more uniform messages;
|
changeset |
files
|
| Mon, 08 Aug 2011 13:19:19 +0200 |
wenzelm |
avoid pointless completion of illegal control commands;
|
changeset |
files
|
| Mon, 08 Aug 2011 08:56:58 +0200 |
nipkow |
removed old expand_fun_eq
|
changeset |
files
|
| Mon, 08 Aug 2011 08:25:28 +0200 |
nipkow |
fixed index entry
|
changeset |
files
|
| Mon, 08 Aug 2011 07:35:42 +0200 |
nipkow |
removed old recdef and types usage
|
changeset |
files
|
| Mon, 08 Aug 2011 07:13:16 +0200 |
nipkow |
merged
|
changeset |
files
|
| Sat, 06 Aug 2011 14:16:23 +0200 |
nipkow |
extended user-level attribute case_names with names for case hypotheses
|
changeset |
files
|
| Mon, 01 Aug 2011 12:08:53 +0200 |
nipkow |
infrastructure for attaching names to hypothesis in cases; realised via the same tag mechanism as case names
|
changeset |
files
|
| Sun, 07 Aug 2011 23:08:07 +0200 |
wenzelm |
workaround for Java 1.7 where javax.swing.JComboBox<E> is generic;
|
changeset |
files
|
| Sun, 07 Aug 2011 23:05:50 +0200 |
wenzelm |
updated version information;
|
changeset |
files
|
| Sun, 07 Aug 2011 18:38:36 +0200 |
wenzelm |
fixed document;
|
changeset |
files
|
| Fri, 05 Aug 2011 23:06:54 +0200 |
haftmann |
tuned order: pushing INF and SUP to Inf and Sup
|
changeset |
files
|
| Fri, 05 Aug 2011 22:58:17 +0200 |
haftmann |
tuned order: pushing INF and SUP to Inf and Sup
|
changeset |
files
|
| Fri, 05 Aug 2011 22:45:57 +0200 |
haftmann |
generalized lemmas to complete lattices
|
changeset |
files
|
| Fri, 05 Aug 2011 17:22:28 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Fri, 05 Aug 2011 16:55:14 +0200 |
Andreas Lochbihler |
replace old SML code generator by new code generator in MicroJava/J
|
changeset |
files
|
| Thu, 04 Aug 2011 16:49:57 +0200 |
kleing |
new state syntax with less conflicts
|
changeset |
files
|
| Fri, 05 Aug 2011 14:16:44 +0200 |
Andreas Lochbihler |
replace old SML code generator by new code generator in MicroJava/JVM and /BV
|
changeset |
files
|
| Fri, 05 Aug 2011 00:14:08 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 04 Aug 2011 20:11:39 +0200 |
haftmann |
more fine-granular instantiation
|
changeset |
files
|
| Thu, 04 Aug 2011 19:29:52 +0200 |
haftmann |
solving duality problem for complete_distrib_lattice; tuned
|
changeset |
files
|
| Thu, 04 Aug 2011 23:21:04 +0200 |
berghofe |
merged
|
changeset |
files
|
| Thu, 04 Aug 2011 17:40:48 +0200 |
berghofe |
Pending FDL types may now be associated with Isabelle types as well.
|
changeset |
files
|
| Thu, 04 Aug 2011 07:33:08 +0200 |
haftmann |
tuned orthography
|
changeset |
files
|
| Thu, 04 Aug 2011 07:31:59 +0200 |
haftmann |
avoid yet unknown fact antiquotation
|
changeset |
files
|
| Thu, 04 Aug 2011 07:31:43 +0200 |
haftmann |
NEWS
|
changeset |
files
|
| Wed, 03 Aug 2011 23:21:53 +0200 |
haftmann |
more specific instantiation
|
changeset |
files
|
| Wed, 03 Aug 2011 23:21:52 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Wed, 03 Aug 2011 23:21:52 +0200 |
haftmann |
class complete_distrib_lattice
|
changeset |
files
|
| Wed, 03 Aug 2011 16:08:02 +0200 |
bulwahn |
NEWS
|
changeset |
files
|
| Wed, 03 Aug 2011 14:24:23 +0200 |
bulwahn |
removing value invocations with the SML code generator
|
changeset |
files
|
| Wed, 03 Aug 2011 13:59:59 +0200 |
bulwahn |
removing the SML evaluator
|
changeset |
files
|
| Wed, 03 Aug 2011 11:09:12 +0200 |
kleing |
fixed wrong isubs in IMP/Types
|
changeset |
files
|
| Tue, 02 Aug 2011 08:28:34 -0700 |
huffman |
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
|
changeset |
files
|
| Tue, 02 Aug 2011 07:36:58 -0700 |
huffman |
NEWS: fix typo
|
changeset |
files
|
| Tue, 02 Aug 2011 13:07:00 +0200 |
krauss |
updated unchecked forward reference
|
changeset |
files
|
| Tue, 02 Aug 2011 12:27:24 +0200 |
krauss |
replaced Nitpick's hardwired basic_ersatz_table by context data
|
changeset |
files
|
| Tue, 02 Aug 2011 12:17:48 +0200 |
krauss |
NEWS
|
changeset |
files
|
| Tue, 02 Aug 2011 11:52:57 +0200 |
krauss |
moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
|
changeset |
files
|
| Tue, 02 Aug 2011 10:36:50 +0200 |
krauss |
moved recdef package to HOL/Library/Old_Recdef.thy
|
changeset |
files
|
| Tue, 02 Aug 2011 10:03:14 +0200 |
krauss |
added dynamic ersatz_table to Nitpick's data slot
|
changeset |
files
|
| Tue, 02 Aug 2011 10:03:12 +0200 |
krauss |
eliminated obsolete recdef/wfrec related declarations
|
changeset |
files
|
| Mon, 01 Aug 2011 20:21:11 +0200 |
kleing |
more consistent naming in IMP/Comp_Rev
|
changeset |
files
|
| Mon, 01 Aug 2011 19:53:30 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sat, 30 Jul 2011 08:24:46 +0200 |
haftmann |
tuned proofs
|
changeset |
files
|
| Fri, 29 Jul 2011 19:47:55 +0200 |
haftmann |
tuned proofs
|
changeset |
files
|
| Mon, 01 Aug 2011 09:31:10 -0700 |
huffman |
new theory HOL/Library/Product_Lattice.thy
|
changeset |
files
|
| Sun, 31 Jul 2011 11:13:38 -0700 |
huffman |
domain package: more informative error message for illegal indirect recursion
|
changeset |
files
|
| Thu, 28 Jul 2011 16:56:14 +0200 |
kleing |
compiler proof cleanup
|
changeset |
files
|
| Thu, 28 Jul 2011 16:32:49 +0200 |
blanchet |
added helpers for "All" and "Ex"
|
changeset |
files
|
| Thu, 28 Jul 2011 16:32:48 +0200 |
blanchet |
put parentheses around non-trivial metis call
|
changeset |
files
|
| Thu, 28 Jul 2011 16:32:39 +0200 |
blanchet |
no needless mangling
|
changeset |
files
|
| Thu, 28 Jul 2011 15:15:26 +0200 |
kleing |
resolved code_pred FIXME in IMP; clearer notation for exec_n
|
changeset |
files
|
| Thu, 28 Jul 2011 11:49:03 +0200 |
blanchet |
clean up temporary directory hack
|
changeset |
files
|
| Thu, 28 Jul 2011 11:43:45 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Thu, 28 Jul 2011 11:43:45 +0200 |
blanchet |
fixed lambda concealing
|
changeset |
files
|
| Thu, 28 Jul 2011 11:43:45 +0200 |
blanchet |
make SML/NJ happy
|
changeset |
files
|
| Thu, 28 Jul 2011 10:42:24 +0200 |
hoelzl |
simplified definition of vector (also removed Cartesian_Euclidean_Space.from_nat which collides with Countable.from_nat)
|
changeset |
files
|
| Thu, 28 Jul 2011 05:52:28 -0200 |
noschinl |
document coercions
|
changeset |
files
|
| Wed, 27 Jul 2011 20:28:00 +0200 |
bulwahn |
rudimentary documentation of the quotient package in the isar reference manual
|
changeset |
files
|
| Wed, 27 Jul 2011 19:35:00 +0200 |
hoelzl |
to_nat is injective on arbitrary domains
|
changeset |
files
|
| Wed, 27 Jul 2011 19:34:30 +0200 |
hoelzl |
finite vimage on arbitrary domains
|
changeset |
files
|
| Tue, 26 Jul 2011 22:53:06 +0200 |
blanchet |
updated Sledgehammer documentation
|
changeset |
files
|
| Tue, 26 Jul 2011 22:53:06 +0200 |
blanchet |
renamed "preds" encodings to "guards"
|
changeset |
files
|
| Tue, 26 Jul 2011 18:11:38 +0200 |
bulwahn |
more precise dependencies
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
further worked around LEO-II parser limitation, with eta-expansion
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly)
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
no need for existential witnesses for sorts in TFF and THF formats
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
mangle "undefined"
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
tuning -- remove useless function (at this point combinators are already in)
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
remove spurious message
|
changeset |
files
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
|
changeset |
files
|
| Tue, 26 Jul 2011 14:50:15 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Tue, 26 Jul 2011 14:05:28 +0200 |
Andreas Lochbihler |
fixed code generator setup in List_Cset
|
changeset |
files
|
| Tue, 26 Jul 2011 13:50:03 +0200 |
hoelzl |
enat is a complete_linorder instance
|
changeset |
files
|
| Tue, 26 Jul 2011 12:44:36 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Tue, 26 Jul 2011 10:49:34 +0200 |
Andreas Lochbihler |
Add theory for setting up monad syntax for Cset
|
changeset |
files
|
| Tue, 26 Jul 2011 11:48:11 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Tue, 26 Jul 2011 08:07:01 +0200 |
bulwahn |
removing expectations from quickcheck example
|
changeset |
files
|
| Tue, 26 Jul 2011 08:07:00 +0200 |
bulwahn |
adding remarks after static inspection of the invocation of the SML code generator
|
changeset |
files
|
| Tue, 26 Jul 2011 10:03:19 +0200 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| Mon, 25 Jul 2011 16:55:48 +0200 |
Andreas Lochbihler |
added operations to Cset with code equations in backing implementations
|
changeset |
files
|
| Mon, 25 Jul 2011 23:27:20 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 25 Jul 2011 23:26:55 +0200 |
haftmann |
adjusted to tailored version of ball_simps
|
changeset |
files
|
| Sun, 24 Jul 2011 22:38:13 +0200 |
haftmann |
adjusted to tailored version of bex_simps
|
changeset |
files
|
| Sun, 24 Jul 2011 21:27:25 +0200 |
haftmann |
more coherent structure in and across theories
|
changeset |
files
|
| Mon, 25 Jul 2011 14:10:12 +0200 |
blanchet |
declare "undefined" constant
|
changeset |
files
|
| Mon, 25 Jul 2011 14:10:12 +0200 |
blanchet |
make compile
|
changeset |
files
|
| Mon, 25 Jul 2011 14:10:12 +0200 |
blanchet |
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
|
changeset |
files
|
| Mon, 25 Jul 2011 14:10:12 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 25 Jul 2011 14:10:12 +0200 |
blanchet |
introduced hybrid lambda translation
|
changeset |
files
|
| Mon, 25 Jul 2011 14:10:12 +0200 |
blanchet |
avoid needless type args for lifted-lambdas
|
changeset |
files
|
| Mon, 25 Jul 2011 11:21:45 +0200 |
bulwahn |
replacing conversion function of old code generator by the current code generator in the reflection tactic
|
changeset |
files
|
| Mon, 25 Jul 2011 11:21:44 +0200 |
bulwahn |
fixed typo
|
changeset |
files
|
| Mon, 25 Jul 2011 10:43:14 +0200 |
bulwahn |
removing SML_Quickcheck
|
changeset |
files
|
| Mon, 25 Jul 2011 10:42:32 +0200 |
bulwahn |
NEWS
|
changeset |
files
|
| Mon, 25 Jul 2011 10:40:52 +0200 |
bulwahn |
added legacy warning to old code generation evaluation
|
changeset |
files
|
| Mon, 25 Jul 2011 10:40:51 +0200 |
bulwahn |
added legacy warning to old code generation commands
|
changeset |
files
|
| Sat, 23 Jul 2011 23:33:59 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 23 Jul 2011 20:05:28 +0200 |
bulwahn |
correcting last example in Predicate_Compile_Examples
|
changeset |
files
|
| Sat, 23 Jul 2011 22:22:21 +0200 |
wenzelm |
make double-sure that interrupts are flushed before executing new work (cf. 22f8c2483bd2);
|
changeset |
files
|
| Sat, 23 Jul 2011 21:29:56 +0200 |
wenzelm |
more detailed tracing;
|
changeset |
files
|
| Sat, 23 Jul 2011 20:34:33 +0200 |
wenzelm |
defensive Term_Sharing, to avoid extending trusted code base of inference kernel;
|
changeset |
files
|
| Sat, 23 Jul 2011 20:11:18 +0200 |
wenzelm |
more precise parse_name according to XML standard;
|
changeset |
files
|
| Sat, 23 Jul 2011 17:22:28 +0200 |
wenzelm |
explicit structure ML_System;
|
changeset |
files
|
| Sat, 23 Jul 2011 16:37:17 +0200 |
wenzelm |
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
|
changeset |
files
|
| Sat, 23 Jul 2011 16:12:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 22 Jul 2011 07:33:34 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 22 Jul 2011 07:33:29 +0200 |
haftmann |
dropped errorneous hint
|
changeset |
files
|
| Thu, 21 Jul 2011 22:47:13 +0200 |
haftmann |
moved some lemmas
|
changeset |
files
|
| Thu, 21 Jul 2011 21:56:24 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 21 Jul 2011 18:40:31 +0200 |
haftmann |
ereal is a complete_linorder instance
|
changeset |
files
|
| Wed, 20 Jul 2011 22:14:39 +0200 |
haftmann |
class complete_linorder
|
changeset |
files
|
| Thu, 21 Jul 2011 21:29:10 +0200 |
blanchet |
make "concealed" lambda translation sound
|
changeset |
files
|
| Thu, 21 Jul 2011 08:33:57 +0200 |
bulwahn |
deactivating all quickcheck invocations until parallel invocation works safely
|
changeset |
files
|
| Thu, 21 Jul 2011 08:31:35 +0200 |
bulwahn |
adapting two examples in Predicate_Compile_Examples
|
changeset |
files
|
| Wed, 20 Jul 2011 23:47:27 +0200 |
blanchet |
use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
|
changeset |
files
|
| Wed, 20 Jul 2011 16:15:33 +0200 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| Wed, 20 Jul 2011 16:14:49 +0200 |
Cezary Kaliszyk |
Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal
|
changeset |
files
|
| Wed, 20 Jul 2011 15:42:23 +0200 |
hoelzl |
add code generator setup and tests for ereal
|
changeset |
files
|
| Wed, 20 Jul 2011 15:09:53 +0200 |
boehmes |
removed debugging facilities accidentally left in the committed code
|
changeset |
files
|
| Wed, 20 Jul 2011 13:29:54 +0200 |
boehmes |
more precise dependencies
|
changeset |
files
|
| Wed, 20 Jul 2011 13:27:01 +0200 |
boehmes |
merged
|
changeset |
files
|
| Wed, 20 Jul 2011 12:23:20 +0200 |
boehmes |
generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
|
changeset |
files
|
| Wed, 20 Jul 2011 09:23:12 +0200 |
boehmes |
moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)
|
changeset |
files
|
| Wed, 20 Jul 2011 09:23:09 +0200 |
boehmes |
removed old (unused) SMT monomorphizer
|
changeset |
files
|
| Wed, 20 Jul 2011 13:24:49 +0200 |
krauss |
added UNION
|
changeset |
files
|
| Wed, 20 Jul 2011 10:48:00 +0200 |
hoelzl |
merged
|
changeset |
files
|
| Tue, 19 Jul 2011 14:38:48 +0200 |
hoelzl |
rename Fin to enat
|
changeset |
files
|
| Tue, 19 Jul 2011 14:38:29 +0200 |
hoelzl |
add ereal to typeclass infinity
|
changeset |
files
|
| Tue, 19 Jul 2011 14:37:49 +0200 |
hoelzl |
add nat => enat coercion
|
changeset |
files
|
| Tue, 19 Jul 2011 14:37:09 +0200 |
hoelzl |
Introduce infinity type class
|
changeset |
files
|
| Tue, 19 Jul 2011 14:36:12 +0200 |
hoelzl |
Rename extreal => ereal
|
changeset |
files
|
| Tue, 19 Jul 2011 14:35:44 +0200 |
hoelzl |
rename Nat_Infinity (inat) to Extended_Nat (enat)
|
changeset |
files
|
| Wed, 20 Jul 2011 10:11:08 +0200 |
Cezary Kaliszyk |
HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
|
changeset |
files
|
| Wed, 20 Jul 2011 08:46:17 +0200 |
kleing |
build an image for HOL-IMP
|
changeset |
files
|
| Wed, 20 Jul 2011 08:16:42 +0200 |
bulwahn |
deactivating quickcheck invocation in this example until the Interrupt issue is understood
|
changeset |
files
|
| Wed, 20 Jul 2011 08:16:41 +0200 |
bulwahn |
removing inner time limits in quickcheck
|
changeset |
files
|
| Wed, 20 Jul 2011 08:16:39 +0200 |
bulwahn |
updating documentation about quickcheck; adding information about try
|
changeset |
files
|
| Wed, 20 Jul 2011 08:16:38 +0200 |
bulwahn |
adapting example in Predicate_Compile_Examples
|
changeset |
files
|
| Wed, 20 Jul 2011 08:16:36 +0200 |
bulwahn |
exporting function in quickcheck; adapting mutabelle script
|
changeset |
files
|
| Wed, 20 Jul 2011 08:16:35 +0200 |
bulwahn |
more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
|
changeset |
files
|
| Wed, 20 Jul 2011 08:16:33 +0200 |
bulwahn |
making messages more informative
|
changeset |
files
|
| Wed, 20 Jul 2011 08:16:32 +0200 |
bulwahn |
only use exhaustive testing in this quickcheck example
|
changeset |
files
|
| Wed, 20 Jul 2011 00:37:42 +0200 |
blanchet |
parse equalities correctly in Nitrox parser
|
changeset |
files
|
| Wed, 20 Jul 2011 00:37:42 +0200 |
blanchet |
pass type arguments to lambda-lifted Frees, to account for polymorphism
|
changeset |
files
|
| Wed, 20 Jul 2011 00:37:42 +0200 |
blanchet |
generate slightly less type information -- this should be sound since type arguments should keep things cleanly apart
|
changeset |
files
|
| Wed, 20 Jul 2011 00:37:42 +0200 |
blanchet |
avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
|
changeset |
files
|
| Wed, 20 Jul 2011 00:37:42 +0200 |
blanchet |
remove offset from Mirabelle output
|
changeset |
files
|
| Tue, 19 Jul 2011 11:15:38 +0200 |
krauss |
the HOL4PROOFS setting is actually HOL4_PROOFS
|
changeset |
files
|
| Tue, 19 Jul 2011 07:14:14 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 18 Jul 2011 21:52:34 +0200 |
haftmann |
proof tuning
|
changeset |
files
|
| Mon, 18 Jul 2011 21:49:39 +0200 |
haftmann |
generalization; various notation and proof tuning
|
changeset |
files
|
| Mon, 18 Jul 2011 21:34:01 +0200 |
haftmann |
avoid misunderstandable names
|
changeset |
files
|
| Mon, 18 Jul 2011 21:15:51 +0200 |
haftmann |
moved lemmas to appropriate theory
|
changeset |
files
|
| Tue, 19 Jul 2011 00:16:18 +0200 |
krauss |
forgotten qualifier
|
changeset |
files
|
| Tue, 19 Jul 2011 00:07:21 +0200 |
krauss |
values_timeout defaults to 600.0 on SML/NJ -- saves us from cluttering all theories equivalent declarations
|
changeset |
files
|
| Mon, 18 Jul 2011 23:48:28 +0200 |
krauss |
killed use of PolyML.makestring
|
changeset |
files
|
| Mon, 18 Jul 2011 23:35:50 +0200 |
krauss |
added experimental mira configuration for HOL Light importer
|
changeset |
files
|
| Mon, 18 Jul 2011 18:52:52 +0200 |
boehmes |
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
|
changeset |
files
|
| Mon, 18 Jul 2011 13:49:26 +0200 |
bulwahn |
unactivating narrowing-based quickcheck by default
|
changeset |
files
|
| Mon, 18 Jul 2011 13:48:35 +0200 |
bulwahn |
making active configuration public in narrowing-based quickcheck
|
changeset |
files
|
| Mon, 18 Jul 2011 11:38:14 +0200 |
bulwahn |
declare tester in this quickcheck example
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adding code equations for partial_term_of for rational numbers
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adapting an experimental setup to changes in quickcheck's infrastructure
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adding narrowing instances for real and rational
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adapting quickcheck based on the analysis of the predicate compiler
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adapting prolog-based tester
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
quickcheck does not deactivate testers if none are given
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
renaming quickcheck_tester to quickcheck_batch_tester; tuned
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
changing parser in quickcheck to activate and deactivate the testers
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adapting SML_Quickcheck to new quickcheck infrastructure
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
enabling parallel execution of testers but removing more informative quickcheck output
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
removing generator registration
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
parametrized test_term functions in quickcheck
|
changeset |
files
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adding random, exhaustive and SML quickcheck as testers
|
changeset |
files
|
| Sun, 17 Jul 2011 22:25:14 +0200 |
haftmann |
more on complement
|
changeset |
files
|
| Sun, 17 Jul 2011 22:24:08 +0200 |
haftmann |
more on complement
|
changeset |
files
|
| Sun, 17 Jul 2011 20:57:56 +0200 |
haftmann |
more consistent theorem names
|
changeset |
files
|
| Sun, 17 Jul 2011 20:46:51 +0200 |
haftmann |
more lemmas about SUP
|
changeset |
files
|
| Sun, 17 Jul 2011 20:29:54 +0200 |
haftmann |
structuring duals together
|
changeset |
files
|
| Sun, 17 Jul 2011 20:23:39 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sun, 17 Jul 2011 20:23:33 +0200 |
haftmann |
more lemmas about Sup
|
changeset |
files
|
| Sun, 17 Jul 2011 19:55:17 +0200 |
haftmann |
generalized INT_anti_mono
|
changeset |
files
|
| Sun, 17 Jul 2011 19:48:02 +0200 |
haftmann |
moving UNIV = ... equations to their proper theories
|
changeset |
files
|
| Sun, 17 Jul 2011 15:15:58 +0200 |
haftmann |
further generalization from sets to complete lattices
|
changeset |
files
|
| Sun, 17 Jul 2011 14:21:19 +0200 |
blanchet |
fixed lambda-liftg: must ensure the formulas are in close form
|
changeset |
files
|
| Sun, 17 Jul 2011 14:12:45 +0200 |
blanchet |
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
|
changeset |
files
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
pass kind to lambda-translation function
|
changeset |
files
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
more refactoring of preprocessing
|
changeset |
files
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
more refactoring of preprocessing, so as to be able to centralize it
|
changeset |
files
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
renamed internal data structure
|
changeset |
files
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
simplify code -- there are no lambdas in helpers anyway
|
changeset |
files
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
added lambda-lifting to Sledgehammer (rough)
|
changeset |
files
|
| Sun, 17 Jul 2011 14:11:34 +0200 |
blanchet |
move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
|
changeset |
files
|
| Sun, 17 Jul 2011 08:45:06 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sat, 16 Jul 2011 22:28:35 +0200 |
haftmann |
generalized some lemmas
|
changeset |
files
|
| Sat, 16 Jul 2011 22:04:02 +0200 |
haftmann |
consolidated bot and top classes, tuned notation
|
changeset |
files
|
| Sat, 16 Jul 2011 21:53:50 +0200 |
haftmann |
tuned notation
|
changeset |
files
|
| Sat, 16 Jul 2011 22:17:27 +0200 |
wenzelm |
clarified bash_output_fifo;
|
changeset |
files
|
| Sat, 16 Jul 2011 20:52:41 +0200 |
wenzelm |
moved bash operations to Isabelle_System (cf. Scala version);
|
changeset |
files
|
| Sat, 16 Jul 2011 20:14:58 +0200 |
wenzelm |
access to process output stream via auxiliary fifo;
|
changeset |
files
|
| Sat, 16 Jul 2011 18:41:35 +0200 |
wenzelm |
some file and directory operations;
|
changeset |
files
|
| Sat, 16 Jul 2011 18:20:02 +0200 |
wenzelm |
more general bash_process, which allows to terminate background processes as well;
|
changeset |
files
|
| Sat, 16 Jul 2011 18:11:14 +0200 |
wenzelm |
updated to Poly/ML SVN 1328, which is considered 5.4.2;
|
changeset |
files
|
| Sat, 16 Jul 2011 17:11:49 +0200 |
wenzelm |
added File.fold_pages for streaming of large files;
|
changeset |
files
|
| Sat, 16 Jul 2011 16:51:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 16 Jul 2011 00:01:17 +0200 |
Cezary Kaliszyk |
HOL/Import: Fix errors with _mk_list
|
changeset |
files
|
| Fri, 15 Jul 2011 16:51:01 +0200 |
wenzelm |
Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de);
|
changeset |
files
|
| Fri, 15 Jul 2011 14:07:12 +0200 |
wenzelm |
simplified malformed YXML markup -- special controls are visible in IsabelleText font;
|
changeset |
files
|
| Fri, 15 Jul 2011 13:29:00 +0200 |
wenzelm |
less ambitious ProofGeneral markup, which occasionally breaks plain-old regexps in elisp;
|
changeset |
files
|
| Fri, 15 Jul 2011 13:28:16 +0200 |
wenzelm |
more robust Binding.pretty/print in typical error sitations with spaces etc. (NB: markup can only provide *additional* emphasis and is occasionally suppressed in TTY mode or tooltips);
|
changeset |
files
|
| Fri, 15 Jul 2011 00:49:38 +0200 |
wenzelm |
more visible printing of empty binding;
|
changeset |
files
|
| Fri, 15 Jul 2011 00:03:47 +0200 |
wenzelm |
do not check vacous bindings, which routinely occur in locale expressions and long theorem statements etc.;
|
changeset |
files
|
| Thu, 14 Jul 2011 23:05:25 +0200 |
wenzelm |
more quotes;
|
changeset |
files
|
| Thu, 14 Jul 2011 22:53:43 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 14 Jul 2011 22:08:11 +0200 |
krauss |
added missing dependencies;
|
changeset |
files
|
| Thu, 14 Jul 2011 19:43:45 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 14 Jul 2011 17:15:24 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 14 Jul 2011 17:14:54 +0200 |
haftmann |
tuned notation and proofs
|
changeset |
files
|
| Thu, 14 Jul 2011 17:29:30 +0200 |
blanchet |
move error logic closer to user
|
changeset |
files
|
| Thu, 14 Jul 2011 17:29:30 +0200 |
blanchet |
allow lambda-lifting without triggers
|
changeset |
files
|
| Thu, 14 Jul 2011 16:50:05 +0200 |
blanchet |
move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
|
changeset |
files
|
| Thu, 14 Jul 2011 16:50:05 +0200 |
blanchet |
added option to control which lambda translation to use (for experiments)
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:38 +0200 |
blanchet |
fix subtle type inference bug in Metis -- different occurrences of the same Skolem might need to be typed differently, using paramify_vars overconstraints the typing problem
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:38 +0200 |
blanchet |
use monomorphic encoding as fallback, since they tend to produce fewer type errors
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:38 +0200 |
blanchet |
don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:37 +0200 |
blanchet |
clearer unsound message
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:37 +0200 |
blanchet |
clarify fine soundness point
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:37 +0200 |
blanchet |
always unfold "Let"s is Sledgehammer, Metis, and MESON
|
changeset |
files
|
| Thu, 14 Jul 2011 15:14:37 +0200 |
blanchet |
unbreak Nitrox's parsing
|
changeset |
files
|
| Thu, 14 Jul 2011 00:21:56 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 14 Jul 2011 00:20:43 +0200 |
haftmann |
tuned lemma positions and proofs
|
changeset |
files
|
| Thu, 14 Jul 2011 00:16:41 +0200 |
haftmann |
tuned notation
|
changeset |
files
|
| Wed, 13 Jul 2011 23:49:56 +0200 |
haftmann |
uniqueness lemmas for bot and top
|
changeset |
files
|
| Wed, 13 Jul 2011 23:41:13 +0200 |
haftmann |
adjusted to tightened specification of classes bot and top
|
changeset |
files
|
| Wed, 13 Jul 2011 19:43:12 +0200 |
haftmann |
moved lemmas bot_less and less_top to classes bot and top respectively
|
changeset |
files
|
| Wed, 13 Jul 2011 19:40:18 +0200 |
haftmann |
tightened specification of classes bot and top: uniqueness of top and bot elements
|
changeset |
files
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
honor the TPTP environment variable as the root of include relative paths -- that's a weird convention but without it Nitrox will fail at CASC
|
changeset |
files
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6
|
changeset |
files
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
more exhaustive testing in Nitrox
|
changeset |
files
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
no timeout for Nitrox
|
changeset |
files
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
avoid relying on piping to "isabelle tty", because this gives errors on some Linuxes about the standard input not being a tty
|
changeset |
files
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
added arithmetic decision procedure to CASC setup
|
changeset |
files
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
added some arithmetic functions, for THF with arithmetic
|
changeset |
files
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
pull in arithmetic theories
|
changeset |
files
|
| Wed, 13 Jul 2011 22:16:19 +0200 |
blanchet |
cleanly separate TPTP related files from other examples
|
changeset |
files
|
| Wed, 13 Jul 2011 21:59:54 +0200 |
bulwahn |
increasing timeout to avoid spurious failures
|
changeset |
files
|
| Wed, 13 Jul 2011 18:36:11 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 13 Jul 2011 07:26:31 +0200 |
haftmann |
more generalization towards complete lattices
|
changeset |
files
|
| Wed, 13 Jul 2011 15:50:45 +0200 |
krauss |
experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
|
changeset |
files
|
| Wed, 13 Jul 2011 04:00:32 +0900 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| Wed, 13 Jul 2011 11:31:36 +0900 |
Cezary Kaliszyk |
Tuned
|
changeset |
files
|
| Thu, 14 Jul 2011 22:30:31 +0200 |
wenzelm |
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;
|
changeset |
files
|
| Wed, 13 Jul 2011 22:05:55 +0200 |
wenzelm |
added term_sharing.ML;
|
changeset |
files
|
| Wed, 13 Jul 2011 21:44:15 +0200 |
wenzelm |
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
|
changeset |
files
|
| Wed, 13 Jul 2011 20:36:18 +0200 |
wenzelm |
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
|
changeset |
files
|
| Wed, 13 Jul 2011 20:13:27 +0200 |
wenzelm |
low-level tuning;
|
changeset |
files
|
| Wed, 13 Jul 2011 16:42:14 +0200 |
wenzelm |
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
|
changeset |
files
|
| Wed, 13 Jul 2011 10:57:09 +0200 |
wenzelm |
XML.pretty with depth limit;
|
changeset |
files
|
| Tue, 12 Jul 2011 23:22:22 +0200 |
wenzelm |
more thorough Variable.check_name: Binding.check for logical entities within the term language;
|
changeset |
files
|
| Tue, 12 Jul 2011 23:20:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 12 Jul 2011 20:53:14 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 13 Jul 2011 00:43:07 +0900 |
Cezary Kaliszyk |
Update HOLLightCompat
|
changeset |
files
|
| Wed, 13 Jul 2011 00:29:33 +0900 |
Cezary Kaliszyk |
Update files generated in HOL/Import/HOLLight
|
changeset |
files
|
| Wed, 13 Jul 2011 00:23:24 +0900 |
Cezary Kaliszyk |
HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems
|
changeset |
files
|
| Tue, 12 Jul 2011 20:11:11 +0200 |
wenzelm |
ML pp for XML.tree;
|
changeset |
files
|
| Tue, 12 Jul 2011 20:11:00 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Tue, 12 Jul 2011 19:49:35 +0200 |
wenzelm |
clarified YXML.detect;
|
changeset |
files
|
| Tue, 12 Jul 2011 19:47:40 +0200 |
wenzelm |
retain some terminology of "XML attributes";
|
changeset |
files
|
| Tue, 12 Jul 2011 19:36:46 +0200 |
wenzelm |
more uniform Properties in ML and Scala;
|
changeset |
files
|
| Tue, 12 Jul 2011 18:00:05 +0200 |
wenzelm |
more uniform Term and Term_XML modules;
|
changeset |
files
|
| Tue, 12 Jul 2011 17:53:06 +0200 |
wenzelm |
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;
|
changeset |
files
|
| Tue, 12 Jul 2011 15:32:16 +0200 |
wenzelm |
tuned signature -- less cryptic ASCII names;
|
changeset |
files
|
| Tue, 12 Jul 2011 15:17:37 +0200 |
wenzelm |
discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;
|
changeset |
files
|
| Tue, 12 Jul 2011 15:12:50 +0200 |
wenzelm |
added Parse.properties (again) -- allow empty list like Parse_Value.properties but unlike Parse.properties of ef86de9c98aa;
|
changeset |
files
|
| Tue, 12 Jul 2011 14:54:29 +0200 |
wenzelm |
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
|
changeset |
files
|
| Tue, 12 Jul 2011 14:33:08 +0200 |
wenzelm |
more precise Symbol_Pos.quote_string;
|
changeset |
files
|
| Tue, 12 Jul 2011 13:45:05 +0200 |
wenzelm |
clarified YXML.embed_controls -- this is idempotent and cannot be nested;
|
changeset |
files
|
| Tue, 12 Jul 2011 13:39:29 +0200 |
wenzelm |
allow empty body for raw_message -- important for Invoke_Scala;
|
changeset |
files
|
| Tue, 12 Jul 2011 11:45:13 +0200 |
wenzelm |
Isabelle string syntax allows literal control characters;
|
changeset |
files
|
| Tue, 12 Jul 2011 11:19:42 +0200 |
wenzelm |
glyphs from DejaVu for ASCII control characters 5, 6, 7, 127, which have a special meaning in Isabelle or Poly/ML;
|
changeset |
files
|
| Tue, 12 Jul 2011 11:16:56 +0200 |
wenzelm |
more precise exceptions;
|
changeset |
files
|
| Tue, 12 Jul 2011 10:44:30 +0200 |
wenzelm |
tuned XML modules;
|
changeset |
files
|
| Tue, 12 Jul 2011 16:00:05 +0900 |
Cezary Kaliszyk |
Quotient example: Lists with distinct elements
|
changeset |
files
|
| Mon, 11 Jul 2011 23:20:40 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 11 Jul 2011 18:44:58 +0200 |
haftmann |
explicit code equation for equality
|
changeset |
files
|
| Mon, 11 Jul 2011 23:15:27 +0200 |
wenzelm |
tuned error messages;
|
changeset |
files
|
| Mon, 11 Jul 2011 23:15:04 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 11 Jul 2011 22:55:47 +0200 |
wenzelm |
tuned signature -- corresponding to Scala version;
|
changeset |
files
|
| Mon, 11 Jul 2011 22:50:29 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Mon, 11 Jul 2011 22:19:11 +0200 |
wenzelm |
more uniform padded_markup, which is important for caret visibility despite absence of markup;
|
changeset |
files
|
| Mon, 11 Jul 2011 17:22:31 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 11 Jul 2011 07:04:30 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sun, 10 Jul 2011 22:42:53 +0200 |
haftmann |
tuned proofs
|
changeset |
files
|
| Sun, 10 Jul 2011 22:17:33 +0200 |
haftmann |
tuned notation
|
changeset |
files
|
| Sun, 10 Jul 2011 22:11:32 +0200 |
haftmann |
tuned notation
|
changeset |
files
|
| Sun, 10 Jul 2011 21:56:39 +0200 |
haftmann |
tuned notation
|
changeset |
files
|
| Mon, 11 Jul 2011 17:22:15 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Mon, 11 Jul 2011 17:14:30 +0200 |
wenzelm |
proper InvocationTargetException.getCause for indirect exceptions;
|
changeset |
files
|
| Mon, 11 Jul 2011 17:11:54 +0200 |
wenzelm |
tuned error message;
|
changeset |
files
|
| Mon, 11 Jul 2011 17:10:32 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 11 Jul 2011 16:48:02 +0200 |
wenzelm |
JVM method invocation service via Scala layer;
|
changeset |
files
|
| Mon, 11 Jul 2011 15:56:30 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 11 Jul 2011 11:13:33 +0200 |
wenzelm |
some support for raw messages, which bypass standard Symbol/YXML decoding;
|
changeset |
files
|
| Mon, 11 Jul 2011 10:27:50 +0200 |
wenzelm |
tuned XML.Cache parameters;
|
changeset |
files
|
| Sun, 10 Jul 2011 23:46:05 +0200 |
wenzelm |
some support to invoke Scala methods under program control;
|
changeset |
files
|
| Sun, 10 Jul 2011 21:46:41 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Sun, 10 Jul 2011 21:39:03 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sun, 10 Jul 2011 15:45:35 +0200 |
haftmann |
tuned proofs and notation
|
changeset |
files
|
| Sun, 10 Jul 2011 14:26:07 +0200 |
haftmann |
more succinct proofs
|
changeset |
files
|
| Sun, 10 Jul 2011 14:14:19 +0200 |
haftmann |
more succinct proofs
|
changeset |
files
|
| Sun, 10 Jul 2011 19:33:27 +0200 |
bulwahn |
adding a very liberal timeout for values after a test case failed due to the restricted timeout
|
changeset |
files
|
| Sun, 10 Jul 2011 14:02:27 +0200 |
bulwahn |
improved NEWS
|
changeset |
files
|
| Sat, 09 Jul 2011 21:18:20 +0200 |
bulwahn |
NEWS
|
changeset |
files
|
| Sat, 09 Jul 2011 21:09:09 +0200 |
bulwahn |
standardized String.concat towards implode (cf. c37a1f29bbc0)
|
changeset |
files
|
| Sat, 09 Jul 2011 19:29:25 +0200 |
bulwahn |
adding quickcheck examples for evaluating floor and ceiling functions
|
changeset |
files
|
| Sat, 09 Jul 2011 19:28:33 +0200 |
bulwahn |
adding code equations to execute floor and ceiling on rational and real numbers
|
changeset |
files
|
| Sat, 09 Jul 2011 13:41:58 +0200 |
bulwahn |
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
|
changeset |
files
|
| Sun, 10 Jul 2011 20:59:04 +0200 |
wenzelm |
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
|
changeset |
files
|
| Sun, 10 Jul 2011 17:58:11 +0200 |
wenzelm |
lambda terms with XML data representation in Scala;
|
changeset |
files
|
| Sun, 10 Jul 2011 16:34:17 +0200 |
wenzelm |
XML data representation of lambda terms;
|
changeset |
files
|
| Sun, 10 Jul 2011 16:31:04 +0200 |
wenzelm |
YXML.string_of_body convenience;
|
changeset |
files
|
| Sun, 10 Jul 2011 16:13:37 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Sun, 10 Jul 2011 16:09:08 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 10 Jul 2011 15:48:15 +0200 |
wenzelm |
more abstract signature;
|
changeset |
files
|
| Sun, 10 Jul 2011 13:51:21 +0200 |
wenzelm |
simplified XML_Data;
|
changeset |
files
|
| Sun, 10 Jul 2011 13:00:22 +0200 |
wenzelm |
less currying in Scala;
|
changeset |
files
|
| Sun, 10 Jul 2011 00:21:19 +0200 |
wenzelm |
propagate header changes to prover process;
|
changeset |
files
|
| Sat, 09 Jul 2011 21:53:27 +0200 |
wenzelm |
echo prover input via raw_messages, for improved protocol tracing;
|
changeset |
files
|
| Sat, 09 Jul 2011 18:54:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 09 Jul 2011 18:35:00 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 09 Jul 2011 18:15:23 +0200 |
wenzelm |
clarified propagation of node name and header;
|
changeset |
files
|
| Sat, 09 Jul 2011 17:14:08 +0200 |
wenzelm |
more precise treatment of prover definedness;
|
changeset |
files
|
| Sat, 09 Jul 2011 16:53:19 +0200 |
wenzelm |
tuned source structure;
|
changeset |
files
|
| Sat, 09 Jul 2011 13:29:33 +0200 |
wenzelm |
some support for blobs (arbitrary text files) within document nodes;
|
changeset |
files
|
| Sat, 09 Jul 2011 12:56:51 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 08 Jul 2011 22:00:53 +0200 |
wenzelm |
moved global state to structure Document (again);
|
changeset |
files
|
| Fri, 08 Jul 2011 21:44:47 +0200 |
wenzelm |
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
|
changeset |
files
|
| Fri, 08 Jul 2011 20:27:09 +0200 |
wenzelm |
less stateful outer_syntax;
|
changeset |
files
|
| Fri, 08 Jul 2011 17:04:38 +0200 |
wenzelm |
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
|
changeset |
files
|
| Fri, 08 Jul 2011 16:13:34 +0200 |
wenzelm |
discontinued special treatment of hard tabulators;
|
changeset |
files
|
| Fri, 08 Jul 2011 16:01:14 +0200 |
wenzelm |
eliminated hard tabs;
|
changeset |
files
|
| Fri, 08 Jul 2011 15:18:28 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 08 Jul 2011 12:18:46 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 07 Jul 2011 21:53:53 +0200 |
nipkow |
added translation to fix critical pair between abbreviations for surj and ~=
|
changeset |
files
|
| Thu, 07 Jul 2011 23:33:14 +0200 |
bulwahn |
floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling
|
changeset |
files
|
| Fri, 08 Jul 2011 15:17:40 +0200 |
wenzelm |
standardized String.concat towards implode;
|
changeset |
files
|
| Fri, 08 Jul 2011 14:37:19 +0200 |
wenzelm |
more abstract Thy_Load.load_file/use_file for external theory resources;
|
changeset |
files
|
| Fri, 08 Jul 2011 13:59:54 +0200 |
wenzelm |
comment;
|
changeset |
files
|
| Fri, 08 Jul 2011 11:50:58 +0200 |
wenzelm |
clarified Thy_Load.digest_file -- read ML files only once;
|
changeset |
files
|
| Fri, 08 Jul 2011 11:13:21 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 07 Jul 2011 23:55:15 +0200 |
wenzelm |
simplified make_option/dest_option;
|
changeset |
files
|
| Thu, 07 Jul 2011 22:04:30 +0200 |
wenzelm |
explicit Document.Node.Header, with master_dir and thy_name;
|
changeset |
files
|
| Thu, 07 Jul 2011 14:10:50 +0200 |
wenzelm |
explicit indication of type Symbol.Symbol;
|
changeset |
files
|
| Thu, 07 Jul 2011 13:48:30 +0200 |
wenzelm |
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
|
changeset |
files
|
| Wed, 06 Jul 2011 23:11:59 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 06 Jul 2011 17:19:34 +0100 |
blanchet |
make SML/NJ happier
|
changeset |
files
|
| Wed, 06 Jul 2011 17:19:34 +0100 |
blanchet |
make SML/NJ happy + tuning
|
changeset |
files
|
| Wed, 06 Jul 2011 17:19:34 +0100 |
blanchet |
moved ATP dependencies to HOL-Plain, where they belong
|
changeset |
files
|
| Wed, 06 Jul 2011 17:19:34 +0100 |
blanchet |
better setup for experimental "z3_atp"
|
changeset |
files
|
| Wed, 06 Jul 2011 17:58:03 +0200 |
krauss |
64bit versions of some mira configurations
|
changeset |
files
|
| Wed, 06 Jul 2011 17:56:58 +0200 |
krauss |
removed unused mira configuration
|
changeset |
files
|
| Wed, 06 Jul 2011 13:57:52 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 06 Jul 2011 13:52:42 +0200 |
bulwahn |
tuning options to avoid spurious isabelle test failures
|
changeset |
files
|
| Wed, 06 Jul 2011 22:02:52 +0200 |
wenzelm |
clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;
|
changeset |
files
|
| Wed, 06 Jul 2011 20:46:06 +0200 |
wenzelm |
prefer Synchronized.var;
|
changeset |
files
|
| Wed, 06 Jul 2011 20:14:13 +0200 |
wenzelm |
tuned errors;
|
changeset |
files
|
| Wed, 06 Jul 2011 13:31:12 +0200 |
wenzelm |
record package: proper configuration options;
|
changeset |
files
|
| Wed, 06 Jul 2011 11:37:29 +0200 |
wenzelm |
just one copy of split_args;
|
changeset |
files
|
| Wed, 06 Jul 2011 09:54:40 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 05 Jul 2011 19:11:29 +0200 |
hoelzl |
rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq
|
changeset |
files
|
| Tue, 05 Jul 2011 17:09:59 +0100 |
nik |
improved translation of lambdas in THF
|
changeset |
files
|
| Tue, 05 Jul 2011 17:09:59 +0100 |
nik |
added generation of lambdas in THF
|
changeset |
files
|
| Tue, 05 Jul 2011 17:09:59 +0100 |
nik |
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
|
changeset |
files
|
| Tue, 05 Jul 2011 23:18:14 +0200 |
wenzelm |
simplified Symbol.iterator: produce strings, which are mostly preallocated;
|
changeset |
files
|
| Tue, 05 Jul 2011 22:43:18 +0200 |
wenzelm |
tuned comment (cf. e9f26e66692d);
|
changeset |
files
|
| Tue, 05 Jul 2011 22:39:15 +0200 |
wenzelm |
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
|
changeset |
files
|
| Tue, 05 Jul 2011 22:38:44 +0200 |
wenzelm |
theory name needs to conform to Path syntax;
|
changeset |
files
|
| Tue, 05 Jul 2011 21:53:59 +0200 |
wenzelm |
hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
|
changeset |
files
|
| Tue, 05 Jul 2011 21:32:48 +0200 |
wenzelm |
prefer space_explode/split_lines as in Isabelle/ML;
|
changeset |
files
|
| Tue, 05 Jul 2011 21:20:24 +0200 |
wenzelm |
Path.split convenience;
|
changeset |
files
|
| Tue, 05 Jul 2011 20:36:49 +0200 |
wenzelm |
get theory from last executation state;
|
changeset |
files
|
| Tue, 05 Jul 2011 19:45:59 +0200 |
wenzelm |
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
|
changeset |
files
|
| Tue, 05 Jul 2011 11:45:48 +0200 |
wenzelm |
clarified cancel_execution/await_cancellation;
|
changeset |
files
|
| Tue, 05 Jul 2011 11:16:37 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Tue, 05 Jul 2011 10:54:05 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 05 Jul 2011 09:54:39 +0200 |
krauss |
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
|
changeset |
files
|
| Mon, 04 Jul 2011 22:25:33 +0200 |
wenzelm |
Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
|
changeset |
files
|
| Mon, 04 Jul 2011 22:11:32 +0200 |
wenzelm |
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
|
changeset |
files
|
| Mon, 04 Jul 2011 20:18:19 +0200 |
wenzelm |
explicit class Counter;
|
changeset |
files
|
| Mon, 04 Jul 2011 16:54:58 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 04 Jul 2011 10:23:46 +0200 |
hoelzl |
the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})
|
changeset |
files
|
| Mon, 04 Jul 2011 10:15:49 +0200 |
hoelzl |
equalities of subsets of atLeastLessThan
|
changeset |
files
|
| Sun, 03 Jul 2011 09:59:25 +0200 |
bulwahn |
adding documentation of the value antiquotation to the code generation manual
|
changeset |
files
|
| Sun, 03 Jul 2011 08:15:14 +0200 |
blanchet |
make SML/NJ happy
|
changeset |
files
|
| Sat, 02 Jul 2011 22:55:58 +0200 |
haftmann |
install case certificate for If after code_datatype declaration for bool
|
changeset |
files
|
| Sat, 02 Jul 2011 22:14:47 +0200 |
haftmann |
tuned typo
|
changeset |
files
|
| Mon, 04 Jul 2011 16:51:45 +0200 |
wenzelm |
pervasive Basic_Library in Scala;
|
changeset |
files
|
| Mon, 04 Jul 2011 16:27:11 +0200 |
wenzelm |
some support for theory files within Isabelle/Scala session;
|
changeset |
files
|
| Mon, 04 Jul 2011 13:43:10 +0200 |
wenzelm |
imitate exception ERROR of Isabelle/ML;
|
changeset |
files
|
| Sun, 03 Jul 2011 19:53:35 +0200 |
wenzelm |
eliminated null;
|
changeset |
files
|
| Sun, 03 Jul 2011 19:42:32 +0200 |
wenzelm |
more explicit edit_node vs. init_node;
|
changeset |
files
|
| Sun, 03 Jul 2011 15:10:17 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 02 Jul 2011 23:31:07 +0200 |
wenzelm |
Thy_Header.read convenience;
|
changeset |
files
|
| Sat, 02 Jul 2011 23:04:19 +0200 |
wenzelm |
some support for Session.File_Store;
|
changeset |
files
|
| Sat, 02 Jul 2011 21:24:19 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 02 Jul 2011 20:54:38 +0200 |
wenzelm |
eliminated redundant session_ready;
|
changeset |
files
|
| Sat, 02 Jul 2011 20:22:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 02 Jul 2011 19:22:06 +0200 |
wenzelm |
uniform finish_thy -- always Global_Theory.join_proofs, even with sequential scheduling;
|
changeset |
files
|
| Sat, 02 Jul 2011 19:08:51 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sat, 02 Jul 2011 10:37:35 +0200 |
haftmann |
correction: do not assume that case const index covered all cases
|
changeset |
files
|
| Fri, 01 Jul 2011 23:31:23 +0200 |
haftmann |
remove illegal case combinators after merge
|
changeset |
files
|
| Fri, 01 Jul 2011 23:10:27 +0200 |
haftmann |
corrected misunderstanding what `old functions` are supposed to be
|
changeset |
files
|
| Fri, 01 Jul 2011 23:07:06 +0200 |
haftmann |
centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be
|
changeset |
files
|
| Fri, 01 Jul 2011 22:48:05 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 01 Jul 2011 19:57:41 +0200 |
haftmann |
index cases for constructors
|
changeset |
files
|
| Fri, 01 Jul 2011 19:42:07 +0200 |
noschinl |
cover induct's "arbitrary" more deeply
|
changeset |
files
|
| Fri, 01 Jul 2011 18:11:17 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Fri, 01 Jul 2011 17:44:04 +0200 |
blanchet |
enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
|
changeset |
files
|
| Fri, 01 Jul 2011 16:31:33 +0200 |
blanchet |
made minimizer informative output accurate
|
changeset |
files
|
| Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
test a few more type encodings
|
changeset |
files
|
| Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
further repair "mangled_tags", now that tags are also mangled
|
changeset |
files
|
| Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
|
changeset |
files
|
| Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
renamed "type_sys" to "type_enc", which is more accurate
|
changeset |
files
|
| Fri, 01 Jul 2011 15:53:37 +0200 |
blanchet |
document "simple_higher" type encoding
|
changeset |
files
|
| Fri, 01 Jul 2011 15:53:37 +0200 |
blanchet |
cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
|
changeset |
files
|
| Fri, 01 Jul 2011 15:53:37 +0200 |
blanchet |
mangle "ti" tags
|
changeset |
files
|
| Fri, 01 Jul 2011 15:53:37 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 01 Jul 2011 17:36:25 +0200 |
wenzelm |
clarified Thy_Syntax.element;
|
changeset |
files
|
| Fri, 01 Jul 2011 16:05:38 +0200 |
wenzelm |
tuned layout;
|
changeset |
files
|
| Fri, 01 Jul 2011 15:16:03 +0200 |
wenzelm |
proper @{binding} antiquotations (relevant for formal references);
|
changeset |
files
|
| Fri, 01 Jul 2011 15:14:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 01 Jul 2011 14:17:02 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 01 Jul 2011 13:54:25 +0200 |
noschinl |
reverted 782991e4180d: fold_fields was never used
|
changeset |
files
|
| Fri, 01 Jul 2011 13:54:23 +0200 |
noschinl |
reverted ce00462f,b3759dce, 7a165592: unwanted generalisation
|
changeset |
files
|
| Fri, 01 Jul 2011 11:26:02 +0200 |
bulwahn |
improving actual dependencies
|
changeset |
files
|
| Fri, 01 Jul 2011 10:45:51 +0200 |
bulwahn |
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
|
changeset |
files
|
| Fri, 01 Jul 2011 10:45:49 +0200 |
bulwahn |
adding a value antiquotation
|
changeset |
files
|
| Thu, 30 Jun 2011 19:24:09 +0200 |
wenzelm |
more general theory header parsing;
|
changeset |
files
|
| Thu, 30 Jun 2011 16:50:26 +0200 |
wenzelm |
back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);
|
changeset |
files
|
| Thu, 30 Jun 2011 16:07:30 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 30 Jun 2011 10:15:46 +0200 |
krauss |
parse term in auxiliary context augmented with variable;
|
changeset |
files
|
| Wed, 29 Jun 2011 11:58:35 +0200 |
boehmes |
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
|
changeset |
files
|
| Thu, 30 Jun 2011 14:55:01 +0200 |
wenzelm |
prefer Isabelle path algebra;
|
changeset |
files
|
| Thu, 30 Jun 2011 14:51:32 +0200 |
wenzelm |
proper fold order;
|
changeset |
files
|
| Thu, 30 Jun 2011 14:03:31 +0200 |
wenzelm |
more Path operations;
|
changeset |
files
|
| Thu, 30 Jun 2011 13:59:55 +0200 |
wenzelm |
getenv_strict in ML;
|
changeset |
files
|
| Thu, 30 Jun 2011 13:21:41 +0200 |
wenzelm |
standardized use of Path operations;
|
changeset |
files
|
| Thu, 30 Jun 2011 11:15:36 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Thu, 30 Jun 2011 00:09:57 +0200 |
wenzelm |
abstract algebra of file paths in Scala (cf. path.ML);
|
changeset |
files
|
| Thu, 30 Jun 2011 00:01:00 +0200 |
wenzelm |
proper Path.print;
|
changeset |
files
|
| Wed, 29 Jun 2011 23:43:48 +0200 |
wenzelm |
basic operations on lists and strings;
|
changeset |
files
|
| Wed, 29 Jun 2011 21:34:16 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 29 Jun 2011 20:39:41 +0200 |
wenzelm |
simplified/unified Simplifier.mk_solver;
|
changeset |
files
|
| Wed, 29 Jun 2011 18:12:34 +0200 |
wenzelm |
modernized some simproc setup;
|
changeset |
files
|
| Wed, 29 Jun 2011 17:35:46 +0200 |
wenzelm |
modernized some simproc setup;
|
changeset |
files
|
| Wed, 29 Jun 2011 16:31:50 +0200 |
wenzelm |
print Path.T with some markup;
|
changeset |
files
|
| Wed, 29 Jun 2011 15:23:36 +0200 |
wenzelm |
HTML: render control symbols more like Isabelle/Scala/jEdit;
|
changeset |
files
|
| Tue, 28 Jun 2011 10:52:15 +0200 |
traytel |
collapse map functions with identity subcoercions to identities;
|
changeset |
files
|
| Tue, 28 Jun 2011 21:06:59 +0200 |
blanchet |
reenabled accidentally-disabled automatic minimization
|
changeset |
files
|
| Tue, 28 Jun 2011 20:42:29 +0200 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Tue, 28 Jun 2011 17:13:32 +0100 |
paulson |
merged
|
changeset |
files
|
| Tue, 28 Jun 2011 17:12:50 +0100 |
paulson |
tidied messy proofs
|
changeset |
files
|
| Tue, 28 Jun 2011 16:43:44 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Tue, 28 Jun 2011 14:36:43 +0200 |
bulwahn |
adding timeout to quickcheck narrowing
|
changeset |
files
|
| Tue, 28 Jun 2011 14:52:46 +0100 |
paulson |
simplified proofs using metis calls
|
changeset |
files
|
| Tue, 28 Jun 2011 12:48:00 +0100 |
paulson |
merged
|
changeset |
files
|
| Tue, 28 Jun 2011 12:47:32 +0100 |
paulson |
keyfree: The set of key-free messages (and associated theorems)
|
changeset |
files
|
| Mon, 27 Jun 2011 22:44:44 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 27 Jun 2011 17:04:04 +0200 |
krauss |
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
|
changeset |
files
|
| Mon, 27 Jun 2011 14:56:39 +0200 |
blanchet |
added reference for MESON
|
changeset |
files
|
| Mon, 27 Jun 2011 14:56:37 +0200 |
blanchet |
document "meson" and "metis" in HOL specific section of the Isar ref manual
|
changeset |
files
|
| Mon, 27 Jun 2011 14:56:35 +0200 |
blanchet |
clarify minimizer output
|
changeset |
files
|
| Mon, 27 Jun 2011 14:56:33 +0200 |
blanchet |
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
|
changeset |
files
|
| Mon, 27 Jun 2011 14:56:32 +0200 |
blanchet |
tweaked comment
|
changeset |
files
|
| Mon, 27 Jun 2011 14:56:31 +0200 |
blanchet |
document "sound" option
|
changeset |
files
|
| Mon, 27 Jun 2011 14:56:29 +0200 |
blanchet |
minor Sledgehammer news
|
changeset |
files
|
| Mon, 27 Jun 2011 14:56:28 +0200 |
blanchet |
added "sound" option to force Sledgehammer to be pedantically sound
|
changeset |
files
|
| Mon, 27 Jun 2011 14:56:26 +0200 |
blanchet |
removed "full_types" option from documentation
|
changeset |
files
|
| Mon, 27 Jun 2011 14:56:10 +0200 |
blanchet |
document changes to Sledgehammer and "try"
|
changeset |
files
|
| Mon, 27 Jun 2011 13:52:47 +0200 |
blanchet |
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
|
changeset |
files
|
| Mon, 27 Jun 2011 13:52:47 +0200 |
blanchet |
clarify warning message to avoid confusing beginners
|
changeset |
files
|
| Mon, 27 Jun 2011 13:52:47 +0200 |
blanchet |
remove experimental trimming feature -- it slowed down things on Linux for some reason
|
changeset |
files
|
| Mon, 27 Jun 2011 13:52:47 +0200 |
blanchet |
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
|
changeset |
files
|
| Mon, 27 Jun 2011 22:23:44 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Mon, 27 Jun 2011 22:20:49 +0200 |
wenzelm |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
changeset |
files
|
| Mon, 27 Jun 2011 17:51:28 +0200 |
wenzelm |
proper checking of @{ML_antiquotation};
|
changeset |
files
|
| Mon, 27 Jun 2011 17:20:24 +0200 |
wenzelm |
hide rather short auxiliary names, which can easily occur in user theories;
|
changeset |
files
|
| Mon, 27 Jun 2011 17:06:06 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
changeset |
files
|
| Mon, 27 Jun 2011 15:03:55 +0200 |
wenzelm |
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
|
changeset |
files
|
| Mon, 27 Jun 2011 15:01:08 +0200 |
wenzelm |
parallel Syntax.parse, which is rather slow;
|
changeset |
files
|
| Mon, 27 Jun 2011 14:38:58 +0200 |
wenzelm |
markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";
|
changeset |
files
|
| Mon, 27 Jun 2011 09:42:46 +0200 |
hoelzl |
move conditional expectation to its own theory file
|
changeset |
files
|
| Sun, 26 Jun 2011 19:10:03 +0200 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Sun, 26 Jun 2011 19:10:02 +0200 |
boehmes |
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
|
changeset |
files
|
| Sat, 25 Jun 2011 20:03:07 +0200 |
wenzelm |
proper tokens only if session is ready;
|
changeset |
files
|
| Sat, 25 Jun 2011 19:38:35 +0200 |
wenzelm |
entity markup for "type", "constant";
|
changeset |
files
|
| Sat, 25 Jun 2011 19:19:13 +0200 |
wenzelm |
clarified Markup.CLASS vs. HTML.CLASS;
|
changeset |
files
|
| Sat, 25 Jun 2011 18:29:51 +0200 |
wenzelm |
tuned color, to avoid confusion with type variables;
|
changeset |
files
|
| Sat, 25 Jun 2011 18:24:52 +0200 |
wenzelm |
discontinued generic XML markup -- this is for XHTML with <span/> elements;
|
changeset |
files
|
| Sat, 25 Jun 2011 18:15:36 +0200 |
wenzelm |
type classes: entity markup instead of old-style token markup;
|
changeset |
files
|
| Sat, 25 Jun 2011 17:17:49 +0200 |
wenzelm |
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
|
changeset |
files
|
| Sat, 25 Jun 2011 15:08:58 +0200 |
wenzelm |
clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example;
|
changeset |
files
|
| Sat, 25 Jun 2011 15:02:12 +0200 |
wenzelm |
produce string constant directly;
|
changeset |
files
|
| Sat, 25 Jun 2011 14:28:43 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 25 Jun 2011 12:19:54 +0200 |
ballarin |
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
|
changeset |
files
|
| Sat, 25 Jun 2011 14:25:10 +0200 |
wenzelm |
removed very slow proof of unnamed/unused theorem from HOL/Quickcheck_Narrowing.thy (cf. 2dee03f192b7) -- can take seconds for main HOL and minutes for HOL-Proofs;
|
changeset |
files
|
| Sat, 25 Jun 2011 12:57:46 +0200 |
wenzelm |
clarified java.ext.dirs: putting Isabelle extensions first makes it work miraculously even on Cygwin with Java in "C:\Program Files\..." (with spaces in file name);
|
changeset |
files
|
| Sat, 25 Jun 2011 12:54:32 +0200 |
wenzelm |
CLASSPATH already converted in isabelle java wrapper;
|
changeset |
files
|
| Sat, 25 Jun 2011 11:51:50 +0200 |
wenzelm |
removed unused/broken Isabelle.exe for now -- needs update of Admin/launch4j;
|
changeset |
files
|
| Thu, 23 Jun 2011 23:12:00 +0200 |
wenzelm |
more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
|
changeset |
files
|
| Thu, 23 Jun 2011 23:05:38 +0200 |
wenzelm |
clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);
|
changeset |
files
|
| Thu, 23 Jun 2011 20:30:48 +0200 |
wenzelm |
more robust concurrent builds;
|
changeset |
files
|
| Thu, 23 Jun 2011 10:08:35 -0700 |
huffman |
merged
|
changeset |
files
|
| Thu, 23 Jun 2011 10:07:16 -0700 |
huffman |
add countable_datatype method for proving countable class instances
|
changeset |
files
|
| Thu, 23 Jun 2011 18:32:13 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Thu, 23 Jun 2011 09:16:48 -0700 |
huffman |
instance inat :: number_semiring
|
changeset |
files
|
| Thu, 23 Jun 2011 09:04:20 -0700 |
huffman |
added number_semiring class, plus a few new lemmas;
|
changeset |
files
|
| Thu, 23 Jun 2011 16:31:20 +0200 |
blanchet |
merged
|
changeset |
files
|
| Thu, 23 Jun 2011 11:19:41 +0200 |
blanchet |
fiddle with remote ATP settings, based on Judgment Day
|
changeset |
files
|
| Thu, 23 Jun 2011 11:19:41 +0200 |
blanchet |
give slightly more time to server to respond, to avoid leaving too much garbage on Geoff's servers
|
changeset |
files
|
| Thu, 23 Jun 2011 12:02:54 +0200 |
ballarin |
Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.
|
changeset |
files
|
| Wed, 22 Jun 2011 15:58:55 -0700 |
huffman |
generalize lemmas power_number_of_even and power_number_of_odd
|
changeset |
files
|
| Wed, 22 Jun 2011 13:45:32 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 22 Jun 2011 13:30:28 -0700 |
huffman |
add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
|
changeset |
files
|
| Thu, 23 Jun 2011 17:17:40 +0200 |
wenzelm |
simplified arrangement of jars;
|
changeset |
files
|
| Thu, 23 Jun 2011 16:34:29 +0200 |
wenzelm |
adapted to Cygwin;
|
changeset |
files
|
| Thu, 23 Jun 2011 16:10:22 +0200 |
wenzelm |
provide Isabelle/Scala environment as Java extension, instead of user classpath
|
changeset |
files
|
| Thu, 23 Jun 2011 14:52:32 +0200 |
wenzelm |
explicit import java.lang.System to prevent odd scope problems;
|
changeset |
files
|
| Thu, 23 Jun 2011 14:48:32 +0200 |
wenzelm |
ensure export of initial CLASSPATH;
|
changeset |
files
|
| Thu, 23 Jun 2011 13:23:00 +0200 |
wenzelm |
augment Java extension directories;
|
changeset |
files
|
| Thu, 23 Jun 2011 10:58:29 +0200 |
wenzelm |
basic setup for Isabelle charset;
|
changeset |
files
|
| Wed, 22 Jun 2011 23:56:44 +0200 |
wenzelm |
prefer actual charset over charset name;
|
changeset |
files
|
| Wed, 22 Jun 2011 21:54:35 +0200 |
wenzelm |
clarified default ML settings;
|
changeset |
files
|
| Wed, 22 Jun 2011 21:35:48 +0200 |
wenzelm |
lazy Isabelle_System.default supports implicit boot;
|
changeset |
files
|
| Wed, 22 Jun 2011 21:27:20 +0200 |
wenzelm |
clarified plugin start/stop;
|
changeset |
files
|
| Wed, 22 Jun 2011 20:56:18 +0200 |
wenzelm |
clarified init/exit procedure;
|
changeset |
files
|
| Wed, 22 Jun 2011 20:38:03 +0200 |
wenzelm |
clarified decoded control symbols;
|
changeset |
files
|
| Wed, 22 Jun 2011 20:25:35 +0200 |
wenzelm |
init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;
|
changeset |
files
|
| Wed, 22 Jun 2011 20:21:22 +0200 |
wenzelm |
prefer STIXGeneral -- hard to tell if better or worse;
|
changeset |
files
|
| Wed, 22 Jun 2011 16:35:31 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 22 Jun 2011 15:07:03 +0200 |
boehmes |
export lambda-lifting code as there is potential use for it within Sledgehammer
|
changeset |
files
|
| Wed, 22 Jun 2011 16:32:36 +0200 |
wenzelm |
updated to jedit-4.4.1 and jedit_build-20110622;
|
changeset |
files
|
| Wed, 22 Jun 2011 16:01:30 +0200 |
wenzelm |
clarified chunk.offset, chunk.length;
|
changeset |
files
|
| Tue, 21 Jun 2011 23:08:16 +0200 |
wenzelm |
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
|
changeset |
files
|
| Tue, 21 Jun 2011 22:40:30 +0200 |
wenzelm |
some arrow symbols from DejaVuSansMono for bsub/esub/bsup/esup;
|
changeset |
files
|
| Tue, 21 Jun 2011 21:34:36 +0200 |
wenzelm |
more precise font transformations: shift sub/superscript, adjust size for user fonts;
|
changeset |
files
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
don't change the way helpers are generated for the exporter's sake
|
changeset |
files
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
provide appropriate type system and number of fact defaults for remote ATPs
|
changeset |
files
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
order generated facts topologically
|
changeset |
files
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
|
changeset |
files
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
tweaked E, SPASS, Vampire setup based on latest Judgment Day results
|
changeset |
files
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
|
changeset |
files
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
avoid double ASCII-fication
|
changeset |
files
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
|
changeset |
files
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
generate type predicates for existentials/skolems, otherwise some problems might not be provable
|
changeset |
files
|
| Tue, 21 Jun 2011 17:17:38 +0200 |
blanchet |
insert rather than append special facts to make it less likely that they're truncated away
|
changeset |
files
|
| Tue, 21 Jun 2011 15:43:27 +0200 |
wenzelm |
hidden font: full height makes cursor more visible;
|
changeset |
files
|
| Tue, 21 Jun 2011 14:12:49 +0200 |
wenzelm |
more uniform treatment of recode_set/recode_map;
|
changeset |
files
|
| Tue, 21 Jun 2011 13:29:44 +0200 |
wenzelm |
tuned iteration over short symbols;
|
changeset |
files
|
| Tue, 21 Jun 2011 12:53:55 +0200 |
wenzelm |
Symbol.is_ctrl: handle decoded version as well;
|
changeset |
files
|
| Tue, 21 Jun 2011 01:08:15 +0200 |
wenzelm |
some support for user symbol fonts;
|
changeset |
files
|
| Mon, 20 Jun 2011 23:25:39 +0200 |
wenzelm |
removed obsolete font specification;
|
changeset |
files
|
| Mon, 20 Jun 2011 23:21:24 +0200 |
wenzelm |
more tolerant Symbol.decode;
|
changeset |
files
|
| Mon, 20 Jun 2011 23:19:38 +0200 |
wenzelm |
simplified/generalized ISABELLE_FONTS handling;
|
changeset |
files
|
| Mon, 20 Jun 2011 22:48:41 +0200 |
wenzelm |
updated to jedit_build-20110620;
|
changeset |
files
|
| Mon, 20 Jun 2011 22:43:56 +0200 |
wenzelm |
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
|
changeset |
files
|
| Mon, 20 Jun 2011 12:13:43 +0200 |
blanchet |
clean up SPASS FLOTTER hack
|
changeset |
files
|
| Mon, 20 Jun 2011 11:42:41 +0200 |
blanchet |
remove automatic recovery from (some) unsound proofs, now that we use sound encodings for all the interesting provers
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
slightly better setup for E
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
respect "really_all" argument, which is used by "ATP_Export"
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
slightly better setup for SPASS and Vampire as more results have come in
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
optimized SPASS and Vampire time slices, like E before
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
optimized E's time slicing, based on latest exhaustive Judgment Day results
|
changeset |
files
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
deal with ATP time slices in a more flexible/robust fashion
|
changeset |
files
|
| Mon, 20 Jun 2011 09:19:31 +0200 |
wenzelm |
literal unicode in README.html allows to copy/paste from Lobo output;
|
changeset |
files
|
| Sun, 19 Jun 2011 22:53:37 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Sun, 19 Jun 2011 22:53:15 +0200 |
wenzelm |
explain special control symbols;
|
changeset |
files
|
| Sun, 19 Jun 2011 22:52:49 +0200 |
wenzelm |
accept control symbols;
|
changeset |
files
|
| Sun, 19 Jun 2011 18:12:49 +0200 |
blanchet |
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
|
changeset |
files
|
| Sun, 19 Jun 2011 18:12:49 +0200 |
blanchet |
recognize one more E failure message
|
changeset |
files
|
| Sun, 19 Jun 2011 18:12:49 +0200 |
blanchet |
tweaked TPTP formula kind for typing information used in the conjecture
|
changeset |
files
|
| Sun, 19 Jun 2011 18:12:49 +0200 |
blanchet |
more forceful message
|
changeset |
files
|
| Sun, 19 Jun 2011 21:53:04 +0200 |
wenzelm |
treat quotes as non-controllable, to reduce surprise in incremental editing;
|
changeset |
files
|
| Sun, 19 Jun 2011 21:47:14 +0200 |
wenzelm |
abbreviations for special control symbols;
|
changeset |
files
|
| Sun, 19 Jun 2011 21:43:41 +0200 |
wenzelm |
completion for control symbols;
|
changeset |
files
|
| Sun, 19 Jun 2011 21:38:48 +0200 |
wenzelm |
updated to jedit_build-20110619;
|
changeset |
files
|
| Sun, 19 Jun 2011 21:34:55 +0200 |
wenzelm |
support for bold style within text buffer;
|
changeset |
files
|
| Sun, 19 Jun 2011 15:31:16 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 19 Jun 2011 15:22:58 +0200 |
wenzelm |
discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);
|
changeset |
files
|
| Sun, 19 Jun 2011 14:36:06 +0200 |
wenzelm |
added glyphs 21e0..21e4, 21e6..21e9, 2759 from DejaVuSansMono;
|
changeset |
files
|
| Sun, 19 Jun 2011 14:31:08 +0200 |
wenzelm |
names for control symbols without "^", which is relevant for completion;
|
changeset |
files
|
| Sun, 19 Jun 2011 14:11:06 +0200 |
wenzelm |
some unicode chars for special control symbols;
|
changeset |
files
|
| Sun, 19 Jun 2011 00:03:44 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 18 Jun 2011 23:51:22 +0200 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Sat, 18 Jun 2011 23:34:34 +0200 |
wenzelm |
avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
|
changeset |
files
|
| Sat, 18 Jun 2011 22:01:22 +0200 |
wenzelm |
proper gfx.setColor;
|
changeset |
files
|
| Sat, 18 Jun 2011 21:26:47 +0200 |
wenzelm |
proper x1;
|
changeset |
files
|
| Sat, 18 Jun 2011 21:20:22 +0200 |
wenzelm |
convenience functions;
|
changeset |
files
|
| Sat, 18 Jun 2011 21:03:52 +0200 |
wenzelm |
more robust caret painting wrt. surrogate characters;
|
changeset |
files
|
| Sat, 18 Jun 2011 18:57:38 +0200 |
wenzelm |
do not control malformed symbols;
|
changeset |
files
|
| Sat, 18 Jun 2011 18:31:55 +0200 |
wenzelm |
Buffer.editSyntaxStyle: mask extended syntax styles;
|
changeset |
files
|
| Sat, 18 Jun 2011 18:17:08 +0200 |
wenzelm |
hardwired abbreviations for standard control symbols;
|
changeset |
files
|
| Sat, 18 Jun 2011 17:42:28 +0200 |
wenzelm |
updated to jedit_build-20110618, which is required for sub/superscript rendering;
|
changeset |
files
|
| Sat, 18 Jun 2011 17:33:27 +0200 |
wenzelm |
basic support for extended syntax styles: sub/superscript;
|
changeset |
files
|
| Sat, 18 Jun 2011 17:32:13 +0200 |
wenzelm |
tuned -- Map.empty serves as partial function;
|
changeset |
files
|
| Sat, 18 Jun 2011 17:30:44 +0200 |
wenzelm |
proper place for config files (cf. 55866987a7d9);
|
changeset |
files
|
| Sat, 18 Jun 2011 15:32:05 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 18 Jun 2011 15:18:57 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 17 Jun 2011 20:38:43 +0200 |
kleing |
IMP compiler with int, added reverse soundness direction
|
changeset |
files
|
| Sat, 18 Jun 2011 15:11:33 +0200 |
wenzelm |
proper place for config files;
|
changeset |
files
|
| Sat, 18 Jun 2011 15:07:16 +0200 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Sat, 18 Jun 2011 14:48:56 +0200 |
wenzelm |
highlight via foreground painter, using alpha channel;
|
changeset |
files
|
| Sat, 18 Jun 2011 12:58:41 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 18 Jun 2011 12:49:55 +0200 |
wenzelm |
tuned text;
|
changeset |
files
|
| Sat, 18 Jun 2011 12:37:42 +0200 |
wenzelm |
inner literal/delimiter corresponds to outer keyword/operator;
|
changeset |
files
|
| Sat, 18 Jun 2011 12:13:42 +0200 |
wenzelm |
tuned markup;
|
changeset |
files
|
| Sat, 18 Jun 2011 11:45:07 +0200 |
wenzelm |
more uniform treatment of "keyword" vs. "operator";
|
changeset |
files
|
| Sat, 18 Jun 2011 11:22:03 +0200 |
wenzelm |
simplified Line_Context (again);
|
changeset |
files
|
| Sat, 18 Jun 2011 00:05:29 +0200 |
wenzelm |
more robust treatment of partial range restriction;
|
changeset |
files
|
| Sat, 18 Jun 2011 00:03:58 +0200 |
wenzelm |
select_markup: no filtering here -- results may be distorted anyway;
|
changeset |
files
|
| Fri, 17 Jun 2011 23:20:34 +0200 |
wenzelm |
more explicit treatment of ranges after revert/convert, which may well distort the overall start/end positions;
|
changeset |
files
|
| Fri, 17 Jun 2011 23:18:22 +0200 |
wenzelm |
more explicit error message;
|
changeset |
files
|
| Fri, 17 Jun 2011 14:35:24 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 16 Jun 2011 13:50:35 +0200 |
blanchet |
gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y"
|
changeset |
files
|
| Thu, 16 Jun 2011 13:50:35 +0200 |
blanchet |
added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users
|
changeset |
files
|
| Thu, 16 Jun 2011 13:50:35 +0200 |
blanchet |
fixed soundness bug related to extensionality
|
changeset |
files
|