make at64 non-experimental

Isabelle process wrapper -- interaction via external program.

Toplevel.loop: explicit argument for secure loop, no warning on quit;

added Isar.secure_main; pass Secure.is_secure to Toplevel.loop;

added Tools/isabelle_process.ML;

isabelle process: replaced option -p by -W (process wrapper);

replaced option -p by -W (process wrapper); tuned PGIP option setup;

\<chi> is now considered a letter; tuned;

symbol chi is also a letter;

improvements

overloading target

interface for unchecked definitions

shifted "fun" command to Wellfounded_Relations

updated

Eliminated unused theorems minusinf_ex and minusinf_bex

first working version of instance target

interpretation for typedefs

using intro_locales instead of unfold_locales if appropriate

more canonical attribute application

adjustions to due to instance target

new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.

*** empty log message ***

added {#.,.,...#}

tuned

stripped down

isabelle-process: option -p echos ISABELLE_PID;

commit: non-critical, otherwise session restart will result in deadlock!

instance command as rudimentary class target

dropped dead code

polyml: default heap size is back to -H 200 (people are still using machines with < 1GB of memory; no need to workaround heap problems of polyml-5.0 anymore);