| Tue, 24 Jul 2012 13:22:06 +0200 |
wenzelm |
tuned messages (cf. isabelle makeall);
|
changeset |
files
|
| Tue, 24 Jul 2012 13:11:50 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Tue, 24 Jul 2012 12:54:34 +0200 |
wenzelm |
actually negate "document" (cf. 7483aa690b4f);
|
changeset |
files
|
| Tue, 24 Jul 2012 12:47:48 +0200 |
wenzelm |
clarified no_build vs. verbose;
|
changeset |
files
|
| Tue, 24 Jul 2012 12:38:33 +0200 |
wenzelm |
clarified "document" again, eliminated redundant "no_document";
|
changeset |
files
|
| Tue, 24 Jul 2012 12:28:20 +0200 |
wenzelm |
clarified build -n (no build);
|
changeset |
files
|
| Tue, 24 Jul 2012 12:20:01 +0200 |
wenzelm |
added "document_dump_only" (cf. negated usedir -C);
|
changeset |
files
|
| Tue, 24 Jul 2012 12:14:16 +0200 |
wenzelm |
more precise propagation of options: build, session, theories;
|
changeset |
files
|
| Tue, 24 Jul 2012 11:39:22 +0200 |
wenzelm |
further imitation of ISABELLE_USEDIR_OPTIONS via options;
|
changeset |
files
|
| Tue, 24 Jul 2012 11:14:37 +0200 |
wenzelm |
observe "condition";
|
changeset |
files
|
| Tue, 24 Jul 2012 11:04:49 +0200 |
wenzelm |
observe "quick_and_dirty";
|
changeset |
files
|
| Tue, 24 Jul 2012 11:02:42 +0200 |
wenzelm |
added "browser_info_remote" (cf. usedir -P);
|
changeset |
files
|
| Tue, 24 Jul 2012 10:58:43 +0200 |
wenzelm |
clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
|
changeset |
files
|
| Tue, 24 Jul 2012 10:44:36 +0200 |
wenzelm |
timing for whole session;
|
changeset |
files
|
| Tue, 24 Jul 2012 10:43:13 +0200 |
wenzelm |
tuned options;
|
changeset |
files
|
| Tue, 24 Jul 2012 10:39:03 +0200 |
wenzelm |
timing is command line options, not system option;
|
changeset |
files
|
| Tue, 24 Jul 2012 10:11:49 +0200 |
wenzelm |
clarified document options;
|
changeset |
files
|
| Tue, 24 Jul 2012 00:29:36 +0200 |
wenzelm |
pass build options to ML;
|
changeset |
files
|
| Mon, 23 Jul 2012 22:35:10 +0200 |
wenzelm |
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
|
changeset |
files
|
| Mon, 23 Jul 2012 21:01:16 +0200 |
wenzelm |
provide explicit ISABELLE_PLATFORM32 as well;
|
changeset |
files
|
| Mon, 23 Jul 2012 19:07:01 +0200 |
berghofe |
merged
|
changeset |
files
|
| Mon, 23 Jul 2012 18:52:10 +0200 |
berghofe |
set_vcs now derives prefix from fully qualified procedure / function name
|
changeset |
files
|
| Mon, 23 Jul 2012 18:21:26 +0200 |
wenzelm |
try droppable application using Platypus functionality -- in contrast to earlier AppHack (cf. 9343d4b7c5bf);
|
changeset |
files
|
| Mon, 23 Jul 2012 18:15:05 +0200 |
wenzelm |
updated to Platypus 4.7;
|
changeset |
files
|
| Mon, 23 Jul 2012 16:44:29 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 23 Jul 2012 16:16:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 23 Jul 2012 16:13:26 +0200 |
wenzelm |
clarified init_component: always liberal;
|
changeset |
files
|
| Mon, 23 Jul 2012 15:59:14 +0200 |
wenzelm |
added system build mode: produce output in ISABELLE_HOME;
|
changeset |
files
|
| Mon, 23 Jul 2012 15:44:42 +0200 |
wenzelm |
removed redundant check (cf. a8ed41b6280b);
|
changeset |
files
|
| Mon, 23 Jul 2012 15:05:05 +0200 |
wenzelm |
pass ISABELLE_BROWSER_INFO as explicit argument;
|
changeset |
files
|
| Mon, 23 Jul 2012 14:18:28 +0200 |
wenzelm |
removed some old/unused stuff;
|
changeset |
files
|
| Mon, 23 Jul 2012 12:05:48 +0200 |
wenzelm |
updated smlnj settings;
|
changeset |
files
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
cap the number of facts returned by MaSh
|
changeset |
files
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
remove MaSh junk associated with size functions
|
changeset |
files
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway
|
changeset |
files
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
removed MaSh junk arising from primrec definitions
|
changeset |
files
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
|
changeset |
files
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
faster "save" operation
|
changeset |
files
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
include unknown local facts in MaSh
|
changeset |
files
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
ensure all calls to "mash" program are synchronous
|
changeset |
files
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
don't relearn old facts in Isar mode
|
changeset |
files
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
|
changeset |
files
|
| Mon, 23 Jul 2012 09:28:03 +0200 |
haftmann |
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
|
changeset |
files
|
| Mon, 23 Jul 2012 09:26:55 +0200 |
haftmann |
more correct import
|
changeset |
files
|
| Sun, 22 Jul 2012 23:36:11 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 22 Jul 2012 10:00:51 +0200 |
haftmann |
NEWS
|
changeset |
files
|
| Sun, 22 Jul 2012 09:56:34 +0200 |
haftmann |
library theories for debugging and parallel computing using code generation towards Isabelle/ML
|
changeset |
files
|
| Sat, 21 Jul 2012 20:01:16 +0200 |
haftmann |
also consider current working directory (cf. 3a5a5a992519)
|
changeset |
files
|
| Sun, 22 Jul 2012 23:31:57 +0200 |
wenzelm |
parallel scheduling of jobs;
|
changeset |
files
|
| Sun, 22 Jul 2012 21:59:14 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 22 Jul 2012 12:26:41 +0200 |
wenzelm |
maintain set of source digests, including relevant parts of session entry;
|
changeset |
files
|
| Sun, 22 Jul 2012 00:00:22 +0200 |
wenzelm |
determine source dependencies, relatively to preloaded theories;
|
changeset |
files
|
| Sat, 21 Jul 2012 22:13:50 +0200 |
wenzelm |
propagate defined options;
|
changeset |
files
|
| Sat, 21 Jul 2012 21:16:08 +0200 |
wenzelm |
disallow quotes in path specifications -- extra paranoia;
|
changeset |
files
|
| Sat, 21 Jul 2012 17:49:22 +0200 |
wenzelm |
save image for inner nodes only;
|
changeset |
files
|
| Sat, 21 Jul 2012 16:41:55 +0200 |
wenzelm |
some actual build function on ML side;
|
changeset |
files
|
| Sat, 21 Jul 2012 12:57:31 +0200 |
wenzelm |
tuned -- no dependency on exit function;
|
changeset |
files
|
| Sat, 21 Jul 2012 12:42:28 +0200 |
wenzelm |
more ML_System operations;
|
changeset |
files
|
| Sat, 21 Jul 2012 10:55:42 +0200 |
bulwahn |
restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs
|
changeset |
files
|
| Sat, 21 Jul 2012 10:53:26 +0200 |
bulwahn |
handling partiality in the case where the equality optimisation is applied
|
changeset |
files
|
| Fri, 20 Jul 2012 23:38:15 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 20 Jul 2012 23:37:54 +0200 |
wenzelm |
updated File.find_files;
|
changeset |
files
|
| Fri, 20 Jul 2012 23:16:54 +0200 |
wenzelm |
more abstract file system operations in Scala, corresponding to ML version;
|
changeset |
files
|
| Fri, 20 Jul 2012 22:39:59 +0200 |
wenzelm |
eliminated obsolete session_manager.scala;
|
changeset |
files
|
| Fri, 20 Jul 2012 22:29:25 +0200 |
wenzelm |
more explicit java.io.{File => JFile};
|
changeset |
files
|
| Fri, 20 Jul 2012 22:43:51 +0200 |
blanchet |
tune Mesh filter
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
faster maximal node computation
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
honor suggested MaSh weights
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
use CVC3 and Yices by default if they are available and there are enough cores
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
relearn ATP proofs
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
don't store fresh names in fact graph, since these cannot be the parents of any other facts
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
added MaSh to news
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
cached ancestor computation
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
minimal maxes + tuning
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn from SMT proofs when they can be minimized by Metis
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
clean up interesting constants a bit
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
convenience
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
name tuning
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learning should honor the fact override and the chained facts
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
MaSh docs
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
added "learn_from_atp" command to MaSh, for patient users
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
get rid of redundant "xxx_INSTALLED" environment variabl
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
add versioning to MaSh state + cleanup dead code
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
eliminated special handling of init case, now that "mash.py" has been optimized to handle sequences of add gracefully
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
more MaSh docs
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
mention MaSh in docs
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
added locality as a MaSh feature
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn command in MaSh
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
added possibility of running external MaSh commands asynchronously
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML structures
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML files
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed "iter" fact filter to "MePo" (Meng--Paulson)
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
handle local facts smoothly in MaSh
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
fixed explosion when computing accessibility
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
|
changeset |
files
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 20 Jul 2012 21:05:47 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 20 Jul 2012 21:04:03 +0200 |
wenzelm |
further imitation of "usedir" shell script;
|
changeset |
files
|
| Fri, 20 Jul 2012 10:53:25 +0200 |
huffman |
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
|
changeset |
files
|
| Thu, 19 Jul 2012 22:21:59 +0200 |
haftmann |
export code relatively to master directory
|
changeset |
files
|
| Fri, 20 Jul 2012 18:50:33 +0200 |
wenzelm |
require explicit initialization of options;
|
changeset |
files
|
| Fri, 20 Jul 2012 17:43:55 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 20 Jul 2012 16:47:43 +0200 |
wenzelm |
define build_options from command line;
|
changeset |
files
|
| Fri, 20 Jul 2012 16:47:17 +0200 |
wenzelm |
some basic Isabelle options;
|
changeset |
files
|
| Fri, 20 Jul 2012 16:45:38 +0200 |
wenzelm |
basic jEdit mode for Isabelle options;
|
changeset |
files
|
| Fri, 20 Jul 2012 15:48:22 +0200 |
wenzelm |
basic support for stand-alone options with external string representation;
|
changeset |
files
|
| Fri, 20 Jul 2012 12:45:12 +0200 |
wenzelm |
minimal build_job;
|
changeset |
files
|
| Fri, 20 Jul 2012 12:27:25 +0200 |
wenzelm |
restrict to required sessions;
|
changeset |
files
|
| Fri, 20 Jul 2012 12:00:08 +0200 |
wenzelm |
proper commas_quote;
|
changeset |
files
|
| Fri, 20 Jul 2012 11:52:20 +0200 |
wenzelm |
tune;
|
changeset |
files
|
| Fri, 20 Jul 2012 11:46:37 +0200 |
wenzelm |
simplified script to build Isabelle/ML;
|
changeset |
files
|
| Thu, 19 Jul 2012 22:32:52 +0200 |
wenzelm |
added eq_file / copy_file corresponding to File.eq / File.copy in ML;
|
changeset |
files
|
| Thu, 19 Jul 2012 20:52:17 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 19 Jul 2012 19:38:39 +0200 |
haftmann |
removed ML module DSeq which was a part of the ancient code generator (cf. 58e33a125f32)
|
changeset |
files
|
| Thu, 19 Jul 2012 12:01:05 +0200 |
bulwahn |
deactivating quickcheck narrowing examples to find out if this causes the system error on the current isatest
|
changeset |
files
|
| Thu, 19 Jul 2012 20:49:17 +0200 |
wenzelm |
support for detached Bash_Job with some control operations;
|
changeset |
files
|
| Thu, 19 Jul 2012 20:39:49 +0200 |
wenzelm |
allow catalog entries to be commented-out;
|
changeset |
files
|
| Thu, 19 Jul 2012 20:02:44 +0200 |
wenzelm |
support external processes with explicit environment;
|
changeset |
files
|
| Thu, 19 Jul 2012 19:12:58 +0200 |
wenzelm |
include COMPONENT/etc/sessions as catalog for more directories, for improved scalability with hundreds of entries (notably AFP);
|
changeset |
files
|
| Thu, 19 Jul 2012 16:09:48 +0200 |
wenzelm |
less redundant data structures;
|
changeset |
files
|
| Thu, 19 Jul 2012 15:45:59 +0200 |
wenzelm |
clarified topological ordering: preserve order of adjacency via reverse fold;
|
changeset |
files
|
| Thu, 19 Jul 2012 14:24:40 +0200 |
wenzelm |
support Session.Queue with ordering and dependencies;
|
changeset |
files
|
| Thu, 19 Jul 2012 14:15:08 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 19 Jul 2012 12:37:08 +0200 |
wenzelm |
more explicit treatment of initial Pure sessions;
|
changeset |
files
|
| Thu, 19 Jul 2012 12:05:54 +0200 |
wenzelm |
more general support for Isabelle/Scala command line tools;
|
changeset |
files
|
| Thu, 19 Jul 2012 11:54:19 +0200 |
wenzelm |
tuned width;
|
changeset |
files
|
| Thu, 19 Jul 2012 11:47:49 +0200 |
wenzelm |
prefer general Properties.Value.Boolean;
|
changeset |
files
|
| Wed, 18 Jul 2012 20:59:02 +0200 |
wenzelm |
more SHA1.digest operations;
|
changeset |
files
|
| Wed, 18 Jul 2012 20:55:19 +0200 |
wenzelm |
tuned import;
|
changeset |
files
|
| Wed, 18 Jul 2012 20:01:55 +0200 |
wenzelm |
tuned source structure;
|
changeset |
files
|
| Wed, 18 Jul 2012 19:47:10 +0200 |
wenzelm |
allow explicit specification of additional session directories;
|
changeset |
files
|
| Wed, 18 Jul 2012 17:27:28 +0200 |
wenzelm |
more errors;
|
changeset |
files
|
| Wed, 18 Jul 2012 17:22:59 +0200 |
wenzelm |
some HOL sessions;
|
changeset |
files
|
| Wed, 18 Jul 2012 17:17:38 +0200 |
wenzelm |
cumulate semantic Session_Info, based on syntactic Session_Entry;
|
changeset |
files
|
| Wed, 18 Jul 2012 16:24:16 +0200 |
wenzelm |
more tight treatment of reset_name;
|
changeset |
files
|
| Wed, 18 Jul 2012 14:07:31 +0200 |
wenzelm |
more informative errors;
|
changeset |
files
|
| Wed, 18 Jul 2012 13:43:36 +0200 |
wenzelm |
added parser for Session_Info;
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:05 +0200 |
blanchet |
repair MaSh exporter
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:05 +0200 |
blanchet |
optimize parent computation in MaSh + remove temporary files
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
make the monomorphizer more predictable by making the cutoff independent on the number of facts
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
speed up MaSh queries
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
attempt at meshing according to more meaningful factors
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
don't include hidden facts in relevance filter + tweak MaSh learning
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
removed debugging output
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
removed expensive HO check in MaSh
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
speed up tautology/metaness check
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
optimized MaSh output by chunking it
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
fixed MaSh state load code so it works even if the facts are read in disorder
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
learn from minimized ATP proofs
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
use async manager to manage MaSh learners to make sure they get killed cleanly
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
more consolidation of MaSh code
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
removed lie
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
drastic overhaul of MaSh data structures + fixed a few performance issues
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
fixed order of accessibles + other tweaks to MaSh
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
added option to control which fact filter is used
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
mesh facts by taking into consideration whether a fact is known to MeSh
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
implemented meshing of Iter and MaSh results
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
implemented MaSh QUERY operation
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
refactored MaSh ADD code so it can be used for SUGGEST as well
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
implemented low-level MaSh ADD operation
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
make tracing an option
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
cleaner handling of metacharacters + freshness of one-off facts
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
better zipping of MaSh facts
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
implemented MaSh learn theory function
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
more work on MaSh
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
improved MaSh string escaping and make more operations string-based
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more implementation work on MaSh
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
started implementing MaSh client-side I/O
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
tweak output
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
centrally construct expensive data structures
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more work on MaSh
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
compile
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
gracefully handle the case of empty theories when going up the accessibility chain
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
doc updates
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
renamed Sledgehammer options
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more code rationalization in relevance filter
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
moved override out of iter filter
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
fixed bug introduced when moving code around
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
systematize lazy names in relevance filter
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
rationalize relevance filter, slowing moving code from Iter to MaSh
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
killed one file
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
dependency tuning
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
renaming
|
changeset |
files
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
clean up dependencies
|
changeset |
files
|
| Tue, 17 Jul 2012 23:11:27 +0200 |
haftmann |
explicitly import Dlist theory into library
|
changeset |
files
|
| Tue, 17 Jul 2012 23:11:24 +0200 |
haftmann |
tuned whitespace
|
changeset |
files
|
| Tue, 17 Jul 2012 23:07:51 +0200 |
haftmann |
dropped ancient example generates
|
changeset |
files
|
| Tue, 17 Jul 2012 22:34:29 +0200 |
wenzelm |
basic support for session ROOT files, with examples for FOL and ZF;
|
changeset |
files
|
| Tue, 17 Jul 2012 21:49:32 +0200 |
wenzelm |
more accurate imitation of formal text;
|
changeset |
files
|
| Tue, 17 Jul 2012 16:56:29 +0200 |
wenzelm |
avoid Source.fromFile, which does not necessarily close its input;
|
changeset |
files
|
| Tue, 17 Jul 2012 16:54:23 +0200 |
wenzelm |
tuned imports;
|
changeset |
files
|
| Tue, 17 Jul 2012 15:56:19 +0200 |
wenzelm |
basic setup for Isabelle build tool;
|
changeset |
files
|
| Tue, 17 Jul 2012 14:33:23 +0200 |
wenzelm |
more standard main method;
|
changeset |
files
|
| Tue, 17 Jul 2012 13:07:28 +0200 |
wenzelm |
avoid slightly odd share_common_data -- Poly/ML 5.5.x should manage low-memory situations (cf. f55e77f623ab);
|
changeset |
files
|
| Tue, 17 Jul 2012 10:39:39 +0200 |
bulwahn |
improved equality optimisation in Quickcheck
|
changeset |
files
|
| Mon, 16 Jul 2012 21:20:56 +0200 |
wenzelm |
more direct Sorts.has_instance;
|
changeset |
files
|
| Mon, 16 Jul 2012 15:57:21 +0200 |
wenzelm |
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
|
changeset |
files
|
| Mon, 16 Jul 2012 15:55:21 +0200 |
wenzelm |
comment;
|
changeset |
files
|
| Mon, 16 Jul 2012 11:26:16 +0200 |
wenzelm |
added universal jdk-6u31.tar.gz component (post Isabelle2012);
|
changeset |
files
|
| Mon, 16 Jul 2012 11:12:06 +0200 |
wenzelm |
more components from Isabelle2011-1 and Isabelle2012;
|
changeset |
files
|
| Mon, 16 Jul 2012 08:44:29 +0200 |
bulwahn |
deactivate Find_Unused_Assms_Examples to see if isabelle test's failures is caused by this example file
|
changeset |
files
|
| Sun, 15 Jul 2012 22:58:52 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Sun, 15 Jul 2012 22:56:49 +0200 |
krauss |
updated versions
|
changeset |
files
|
| Sun, 15 Jul 2012 22:31:31 +0200 |
krauss |
added component integrity checks and some initial checksums
|
changeset |
files
|
| Sun, 15 Jul 2012 17:53:47 +0200 |
wenzelm |
prefer canonical fold_rev;
|
changeset |
files
|
| Sun, 15 Jul 2012 17:27:19 +0200 |
wenzelm |
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
|
changeset |
files
|
| Sun, 15 Jul 2012 16:53:50 +0200 |
wenzelm |
tuned proof;
|
changeset |
files
|
| Sun, 15 Jul 2012 16:44:40 +0200 |
wenzelm |
more precise imports;
|
changeset |
files
|
| Sat, 14 Jul 2012 21:15:41 +0200 |
wenzelm |
removed some old/unused stuff;
|
changeset |
files
|
| Sat, 14 Jul 2012 21:05:29 +0200 |
wenzelm |
actually remove former atbroy102/cygwin stuff (cf. 6301046146b6, 08cb859c53cd);
|
changeset |
files
|
| Sat, 14 Jul 2012 20:59:49 +0200 |
wenzelm |
more user aliases;
|
changeset |
files
|
| Sat, 14 Jul 2012 16:35:58 +0200 |
nipkow |
removed superfluous lemmas
|
changeset |
files
|
| Fri, 13 Jul 2012 08:45:09 +0200 |
bulwahn |
fixed typo
|
changeset |
files
|
| Fri, 13 Jul 2012 08:44:42 +0200 |
bulwahn |
renaming the example file which was overlooked before
|
changeset |
files
|
| Thu, 12 Jul 2012 16:22:33 +0200 |
bulwahn |
a first guess to avoid the Codegenerator_Test to loop infinitely
|
changeset |
files
|
| Thu, 12 Jul 2012 21:46:11 +1000 |
Gerwin Klein |
get attachments sent even on lxbroy Gentoo machines
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
moved most of MaSh exporter code to Sledgehammer
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
dummy implementation
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
split relevance filter code into three files
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
add Isabelle dependencies to tweak relevance filter
|
changeset |
files
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
generate ATP dependencies
|
changeset |
files
|
| Wed, 11 Jul 2012 13:59:39 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 11 Jul 2012 13:54:37 +0200 |
bulwahn |
adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
|
changeset |
files
|
| Wed, 11 Jul 2012 11:28:27 +0200 |
blanchet |
comment
|
changeset |
files
|
| Wed, 11 Jul 2012 11:28:10 +0200 |
blanchet |
nicer output
|
changeset |
files
|
| Wed, 11 Jul 2012 09:32:29 +0200 |
blanchet |
rationalized output
|
changeset |
files
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
generate Meng--Paulson facts for evaluation purposes
|
changeset |
files
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
export useful functions
|
changeset |
files
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
instantiate induction rules
|
changeset |
files
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
MaSh evaluation driver
|
changeset |
files
|