| Wed, 23 Mar 2011 10:18:42 +0100 |
blanchet |
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
|
changeset |
files
|
| Wed, 23 Mar 2011 10:06:27 +0100 |
blanchet |
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
|
changeset |
files
|
| Wed, 23 Mar 2011 10:21:29 +0100 |
boehmes |
really be quiet
|
changeset |
files
|
| Wed, 23 Mar 2011 09:15:49 +0100 |
krauss |
replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH
|
changeset |
files
|
| Tue, 22 Mar 2011 21:22:50 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 22 Mar 2011 20:06:10 +0100 |
hoelzl |
standardized headers
|
changeset |
files
|
| Tue, 22 Mar 2011 18:53:05 +0100 |
hoelzl |
generalized Caratheodory from algebra to ring_of_sets
|
changeset |
files
|
| Tue, 22 Mar 2011 16:44:57 +0100 |
hoelzl |
add ring_of_sets and subset_class as basis for algebra
|
changeset |
files
|
| Tue, 22 Mar 2011 19:04:32 +0100 |
blanchet |
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
|
changeset |
files
|
| Tue, 22 Mar 2011 18:38:29 +0100 |
blanchet |
added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
|
changeset |
files
|
| Tue, 22 Mar 2011 18:27:47 +0100 |
blanchet |
remove lie from documentation
|
changeset |
files
|
| Tue, 22 Mar 2011 17:20:54 +0100 |
blanchet |
let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
|
changeset |
files
|
| Tue, 22 Mar 2011 17:20:53 +0100 |
blanchet |
make Minimizer honor "verbose" and "debug" options better
|
changeset |
files
|
| Tue, 22 Mar 2011 12:49:07 +0100 |
nipkow |
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
|
changeset |
files
|
| Mon, 21 Mar 2011 21:10:29 +0100 |
krauss |
moved some configurations to AFP, and fixed others
|
changeset |
files
|
| Tue, 22 Mar 2011 20:44:47 +0100 |
wenzelm |
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
|
changeset |
files
|
| Tue, 22 Mar 2011 18:03:28 +0100 |
wenzelm |
enable inner syntax source positions by default (controlled via configuration option);
|
changeset |
files
|
| Tue, 22 Mar 2011 17:51:15 +0100 |
wenzelm |
binder_tr: more informative exception;
|
changeset |
files
|
| Tue, 22 Mar 2011 16:39:34 +0100 |
wenzelm |
Hoare syntax: strip positions where they crash translation functions;
|
changeset |
files
|
| Tue, 22 Mar 2011 16:15:50 +0100 |
wenzelm |
update_name_tr: more precise handling of explicit constraints, including positions;
|
changeset |
files
|
| Tue, 22 Mar 2011 15:32:47 +0100 |
wenzelm |
statespace syntax: strip positions -- type constraints are unexpected here;
|
changeset |
files
|
| Tue, 22 Mar 2011 14:45:48 +0100 |
wenzelm |
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
|
changeset |
files
|
| Tue, 22 Mar 2011 14:22:40 +0100 |
wenzelm |
datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
|
changeset |
files
|
| Tue, 22 Mar 2011 13:55:39 +0100 |
wenzelm |
tuned indendation and parentheses;
|
changeset |
files
|
| Tue, 22 Mar 2011 13:32:20 +0100 |
wenzelm |
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
|
changeset |
files
|
| Tue, 22 Mar 2011 11:14:33 +0100 |
wenzelm |
pretty_string: proper handling of negative max_len;
|
changeset |
files
|
| Mon, 21 Mar 2011 23:38:32 +0100 |
wenzelm |
added Lexicon.encode_position, Lexicon.decode_position;
|
changeset |
files
|
| Mon, 21 Mar 2011 21:16:39 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 21 Mar 2011 21:05:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 21 Mar 2011 20:56:44 +0100 |
wenzelm |
clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;
|
changeset |
files
|
| Mon, 21 Mar 2011 20:15:03 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 21 Mar 2011 17:14:52 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 21 Mar 2011 16:24:52 +0100 |
krauss |
added judgement day configurations
|
changeset |
files
|
| Mon, 21 Mar 2011 16:38:28 +0100 |
wenzelm |
another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);
|
changeset |
files
|
| Mon, 21 Mar 2011 14:46:59 +0100 |
krauss |
fixed perl error
|
changeset |
files
|
| Mon, 21 Mar 2011 14:37:10 +0100 |
krauss |
eliminated unnecessary generated ROOT.ML
|
changeset |
files
|
| Mon, 21 Mar 2011 14:25:59 +0100 |
krauss |
more precise dependencies
|
changeset |
files
|
| Mon, 21 Mar 2011 12:43:26 +0100 |
krauss |
small test case for main mirabelle functionality, which easily breaks without noticing
|
changeset |
files
|
| Mon, 21 Mar 2011 12:43:25 +0100 |
krauss |
propagate mirabelle failures properly;
|
changeset |
files
|
| Mon, 21 Mar 2011 12:43:23 +0100 |
krauss |
mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)
|
changeset |
files
|
| Mon, 21 Mar 2011 08:29:16 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adapting predicate_compile_quickcheck; tuned
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adapting mutabelle
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adapting SML_Quickcheck
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
extending the test data generators to take the evaluation terms as arguments
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding option of evaluating terms after invocation in quickcheck
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding eval option to quickcheck
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding a simple datatype for representing functions in Quickcheck_Narrowing
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
extending code_int type more; adding narrowing instance for type int; added test case for int instance
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
|
changeset |
files
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adding size as static argument in quickcheck_narrowing compilation
|
changeset |
files
|
| Sun, 20 Mar 2011 23:07:06 +0100 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:48:08 +0100 |
wenzelm |
dropped unused structure aliases;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:47:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:26:43 +0100 |
wenzelm |
NEWS: structure Timing provides various operations for timing;
|
changeset |
files
|
| Sun, 20 Mar 2011 22:08:12 +0100 |
wenzelm |
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
|
changeset |
files
|
| Sun, 20 Mar 2011 21:44:38 +0100 |
wenzelm |
pure Timing.timing, without any exception handling;
|
changeset |
files
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
changeset |
files
|
| Sun, 20 Mar 2011 21:20:07 +0100 |
wenzelm |
pervasive cond_timeit;
|
changeset |
files
|
| Sun, 20 Mar 2011 20:20:41 +0100 |
wenzelm |
eliminated dead code;
|
changeset |
files
|
| Sun, 20 Mar 2011 20:05:43 +0100 |
wenzelm |
parallel preparation of document variants, within separate directories;
|
changeset |
files
|
| Sun, 20 Mar 2011 19:47:26 +0100 |
wenzelm |
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
|
changeset |
files
|
| Sun, 20 Mar 2011 19:34:18 +0100 |
wenzelm |
eliminated redundant doc_prefix1;
|
changeset |
files
|
| Sun, 20 Mar 2011 19:10:09 +0100 |
wenzelm |
renamed doc_prefix2 to dump_prefix;
|
changeset |
files
|
| Sun, 20 Mar 2011 18:56:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 20 Mar 2011 18:09:32 +0100 |
wenzelm |
tuned terminology for document variants;
|
changeset |
files
|
| Sun, 20 Mar 2011 17:40:45 +0100 |
wenzelm |
replaced File.check by specific File.check_file, File.check_dir;
|
changeset |
files
|
| Sun, 20 Mar 2011 13:49:21 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 19 Mar 2011 14:03:13 +0100 |
blanchet |
preencode value of "need" selectors in Kodkod bounds as an optimization
|
changeset |
files
|
| Sat, 19 Mar 2011 11:22:23 +0100 |
blanchet |
ignore "need" axioms for "nat"-like types
|
changeset |
files
|
| Fri, 18 Mar 2011 22:55:28 +0100 |
blanchet |
added "simp:", "intro:", and "elim:" to "try" command
|
changeset |
files
|
| Fri, 18 Mar 2011 17:27:28 +0100 |
blanchet |
optimize Kodkod axioms further w.r.t. "need" option
|
changeset |
files
|
| Fri, 18 Mar 2011 12:20:32 +0100 |
blanchet |
optimize Kodkod bounds of nat-like datatypes
|
changeset |
files
|
| Fri, 18 Mar 2011 12:05:23 +0100 |
blanchet |
more optimizations of bounds for "need"
|
changeset |
files
|
| Fri, 18 Mar 2011 11:43:28 +0100 |
blanchet |
optimize Kodkod bounds when "need" is specified
|
changeset |
files
|
| Fri, 18 Mar 2011 10:17:37 +0100 |
blanchet |
always destroy constructor patterns, since this seems to be always useful
|
changeset |
files
|
| Thu, 17 Mar 2011 22:07:17 +0100 |
blanchet |
reintroduced "show_skolems" option -- useful when too many Skolems are displayed
|
changeset |
files
|
| Thu, 17 Mar 2011 14:43:53 +0100 |
blanchet |
reword Nitpick's wording concerning potential counterexamples
|
changeset |
files
|
| Thu, 17 Mar 2011 14:43:51 +0100 |
blanchet |
prevent an exception if "card" is empty (e.g., "nitpick [card]")
|
changeset |
files
|
| Thu, 17 Mar 2011 11:18:31 +0100 |
blanchet |
add option to function to keep trivial ATP formulas, needed for some experiments
|
changeset |
files
|
| Thu, 17 Mar 2011 11:18:31 +0100 |
blanchet |
add option to relevance filter's "all_facts" function to really get all facts (needed for some experiments)
|
changeset |
files
|
| Thu, 17 Mar 2011 09:58:13 +0100 |
nipkow |
tuned lemma
|
changeset |
files
|
| Wed, 16 Mar 2011 19:50:56 +0100 |
nipkow |
added lemmas
|
changeset |
files
|
| Tue, 15 Mar 2011 22:04:02 +0100 |
nipkow |
added lemma
|
changeset |
files
|
| Tue, 15 Mar 2011 15:49:42 +0100 |
blanchet |
support non-ground "need" values
|
changeset |
files
|
| Tue, 15 Mar 2011 13:03:54 +0100 |
wenzelm |
recover Isabelle symlink for public distribution, notably website;
|
changeset |
files
|
| Mon, 14 Mar 2011 16:59:37 +0100 |
wenzelm |
standardized headers;
|
changeset |
files
|
| Mon, 14 Mar 2011 15:29:10 +0100 |
hoelzl |
merged
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:49 +0100 |
hoelzl |
reworked Probability theory: measures are not type restricted to positive extended reals
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:47 +0100 |
hoelzl |
split Extended_Reals into parts for Library and Multivariate_Analysis
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:46 +0100 |
hoelzl |
lemmas about addition, SUP on countable sets and infinite sums for extreal
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:45 +0100 |
hoelzl |
add infinite sums and power on extreal
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:44 +0100 |
hoelzl |
introduce setsum on extreal
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:42 +0100 |
hoelzl |
use abs_extreal
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:41 +0100 |
hoelzl |
simplified definition of open_extreal
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:40 +0100 |
hoelzl |
use case_product for extrel[2,3]_cases
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:39 +0100 |
hoelzl |
add Extended_Reals from AFP/Lower_Semicontinuous
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:37 +0100 |
hoelzl |
add lemmas for monotone sequences
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:36 +0100 |
hoelzl |
add lemmas for SUP and INF
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:35 +0100 |
hoelzl |
generalize infinite sums
|
changeset |
files
|
| Mon, 14 Mar 2011 14:37:33 +0100 |
hoelzl |
moved t2_spaces to HOL image
|
changeset |
files
|
| Mon, 14 Mar 2011 15:17:10 +0100 |
wenzelm |
example settings for ISABELLE_GHC, ISABELLE_OCAML, ISABELLE_SWIPL;
|
changeset |
files
|
| Mon, 14 Mar 2011 15:13:00 +0100 |
wenzelm |
isatest: fresh copy of settings avoids odd cumulative environment;
|
changeset |
files
|
| Mon, 14 Mar 2011 12:34:12 +0100 |
bulwahn |
tuned exhaustive_generators
|
changeset |
files
|
| Mon, 14 Mar 2011 12:34:11 +0100 |
bulwahn |
removing definition of cons0; hiding constants in Quickcheck_Narrowing
|
changeset |
files
|
| Mon, 14 Mar 2011 12:34:10 +0100 |
bulwahn |
tuned subsubsection names in Quickcheck_Narrowing
|
changeset |
files
|
| Mon, 14 Mar 2011 12:34:10 +0100 |
bulwahn |
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
|
changeset |
files
|
| Mon, 14 Mar 2011 12:34:09 +0100 |
bulwahn |
correcting names in Narrowing_Engine and example theory for Quickcheck_Narrowing
|
changeset |
files
|
| Mon, 14 Mar 2011 12:34:08 +0100 |
bulwahn |
renaming series and serial to narrowing in Quickcheck_Narrowing
|
changeset |
files
|
| Sun, 13 Mar 2011 23:12:38 +0100 |
wenzelm |
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
|
changeset |
files
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
changeset |
files
|
| Sun, 13 Mar 2011 22:24:10 +0100 |
wenzelm |
eliminated hard tabs;
|
changeset |
files
|
| Sun, 13 Mar 2011 21:41:44 +0100 |
wenzelm |
less ambitious isatest;
|
changeset |
files
|
| Sun, 13 Mar 2011 21:21:48 +0100 |
wenzelm |
modernized imports (untested!?);
|
changeset |
files
|
| Sun, 13 Mar 2011 20:56:00 +0100 |
wenzelm |
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
|
changeset |
files
|
| Sun, 13 Mar 2011 20:21:24 +0100 |
wenzelm |
explicit type SHA1.digest;
|
changeset |
files
|
| Sun, 13 Mar 2011 19:27:39 +0100 |
wenzelm |
slightly more robust bash exec, which fails on empty executable;
|
changeset |
files
|