observe "condition";

observe "quick_and_dirty";

added "browser_info_remote" (cf. usedir -P);

clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;

timing for whole session;

tuned options;

timing is command line options, not system option;

clarified document options;

pass build options to ML; some imitation of usedir Session.init;

added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);

provide explicit ISABELLE_PLATFORM32 as well; discontinued some obsolete platforms; explicit error for unknown platform;

merged

set_vcs now derives prefix from fully qualified procedure / function name

try droppable application using Platypus functionality -- in contrast to earlier AppHack (cf. 9343d4b7c5bf);

updated to Platypus 4.7;

merged

tuned;

clarified init_component: always liberal; reduced divergence of clone from lib/scripts/getsettings;

added system build mode: produce output in ISABELLE_HOME; determine output location more explicitly;

removed redundant check (cf. a8ed41b6280b);

pass ISABELLE_BROWSER_INFO as explicit argument;

removed some old/unused stuff;

updated smlnj settings;

cap the number of facts returned by MaSh

remove MaSh junk associated with size functions

identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway

removed MaSh junk arising from primrec definitions

distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh

tuning

faster "save" operation

include unknown local facts in MaSh

ensure all calls to "mash" program are synchronous

don't relearn old facts in Isar mode

took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks

restrict unqualified imports from Haskell Prelude to a small set of fundamental operations

more correct import

merged

NEWS

library theories for debugging and parallel computing using code generation towards Isabelle/ML

also consider current working directory (cf. 3a5a5a992519)

parallel scheduling of jobs; misc tuning;

tuned;

maintain set of source digests, including relevant parts of session entry;

determine source dependencies, relatively to preloaded theories; tuned signature;

propagate defined options; misc tuning;

disallow quotes in path specifications -- extra paranoia;

save image for inner nodes only; misc tuning and simplification;

some actual build function on ML side; further imitation of "usedir" shell script;

tuned -- no dependency on exit function;

more ML_System operations;

restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs

handling partiality in the case where the equality optimisation is applied

merged

updated File.find_files;

more abstract file system operations in Scala, corresponding to ML version;

eliminated obsolete session_manager.scala;

more explicit java.io.{File => JFile};

tune Mesh filter

faster maximal node computation

honor suggested MaSh weights

use CVC3 and Yices by default if they are available and there are enough cores

relearn ATP proofs

don't store fresh names in fact graph, since these cannot be the parents of any other facts

added MaSh to news

cached ancestor computation

minimal maxes + tuning

learn from SMT proofs when they can be minimized by Metis

clean up interesting constants a bit

convenience

name tuning

learning should honor the fact override and the chained facts

fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully

MaSh docs

added "learn_from_atp" command to MaSh, for patient users

get rid of redundant "xxx_INSTALLED" environment variabl

add versioning to MaSh state + cleanup dead code

eliminated special handling of init case, now that "mash.py" has been optimized to handle sequences of add gracefully

more MaSh docs

mention MaSh in docs

use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them

added locality as a MaSh feature

learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds

learn command in MaSh

added possibility of running external MaSh commands asynchronously

renamed ML structures

renamed ML files

renamed "iter" fact filter to "MePo" (Meng--Paulson)

handle local facts smoothly in MaSh

fixed explosion when computing accessibility

use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)

tuning

merged

further imitation of "usedir" shell script; Pure/build observes build_images option, unlike traditional version; tuned signature;

make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests

export code relatively to master directory

require explicit initialization of options; more explicit Position operations;