update instance proofs to new style

declare sprodE as cases rule; new induction rule sprod_induct

add induction rule ssum_induct

eval_wrapper: CRITICAL; tuned;

try_ml_file: setmp explicit theory context, prevents race condition wrt. concurrent ML_Context.set_context;

tuned spaces;

removed separate exists/forall code;

tuned proofs and comments

removed obsolete banner;

tuned;

added PROMPT message;

added isSystem; tune isRaw;

simple make script;

tuned comments (javadoc);

use polyml-cvs, the 5.2 development branch;

tuned RandomWord interface;

added int/real/list operations; tuned interface; tuned;

use random_word.ML earlier;

changed type definition to make Iwhen and reasoning about chains unnecessary; rearranged sections

Fixed eta constraction issue in compose_witness

included meson/metis tests in simultaneous use_thys;

``print mode'' is now a thread-local value derived from a global template;

scheduling/next_task: PrintMode.closure;

added get/put_data;

separated into global template vs. thread-local value; made setmp thread-local (non-critical); added closure;

Universal values via tagged union. Emulates structure Universal in Poly/ML 5.1.

added ML-Systems/universal.ML;

updated;

obsolete;

removed obsolete (slow!) Random implementation;

moved Pure/General/random_word.ML to Tools/random_word.ML;

adapted theory name;

* Metis prover an order of magnitude faster, works with multithreading.

updated HOL-Nominal-Examples deps;

made refute non-critical (seems to work after avoiding floating point random numbers);

move bottom-related stuff back into Pcpo.thy

polishing of some proofs

Random.range_real makes SML/NJ happy;

tuned comments;

tuned RandomWord signature;

removed strange MacRoman character;

using RandomWord from Isabelle/Pure gains factor 10-20 speedup;

updated;

added General/random_word.ML;

Simple generator for pseudo-random numbers, using unboxed word arithmetic only.

removed duplicate CRITICAL markup;

instantiation target

tuned primitive inferences

Replaced refs by config params; finer critical section in mets method

simultaneous use_thys;

marked refute (the main metis procedure) as CRITICAL;

more examples

accomodate to replacement of K_record by %x.c

replaced K_record by lambda term %x. c

signature BASIC_MULTITHREADING; added specific serial number generator, which avoid the global CRITICAL lock;

removed obsolete use_noncritical (plain use is already non-critical);

serial: now based on specific version in structure Multithreading;

add class ppo of pointed partial orders; define UU in class ppo instead of pcpo; add new lemmas about lub

named some critical sections; eval_antiquotes: tightened critical section;

named some critical sections;

use_text/use_file: non-critical (Poly/ML compiler is thread-safe);

non-critical (accidental concurrent access does not affect functional integrity);

PrintMode.setmp (avoid direct access to print_mode ref);

rearrange into subsections

Skolemization now catches exception THM, which may be raised if unification fails.

Deleted redundant setmp calls

tuned proofs, document;

switched from PreList to ATP_Linkup

Renamed *.size to prod.size.

Alternative names are now also used when storing theorems for size functions.

temporarily fixed documentation due to changed size functions

split_primel: salvaged original proof after blow with sledghammer (this constructive version is required in HOL/Extraction);

cond_timeit: added message argument, use Exn.capture/release; tuned;

cond_timeit: added message argument;

note in target

maior tuning

tuned

Added foldl1.

Adapted to changes in size function.

size functions for nested datatypes are now expressed using generic ..._size functions.

Adapted to changes in interface of indtac.

- Removed redundant head_len field in datatype_info - Added new alt_names field in datatype_info

- Removed redundant head_len field in datatype_info - Added new alt_names field in datatype_info - indtac now takes additional list of variables as argument

tidied some messy proofs

Deleted copy of indtac.

Added code lemma for message_string_size.

Removed obsolete lemma size_sum.

fixed ancestors

whitespace typo

explicit closing of derived witnesses

closed rules

improved semantics of timeapp_msg

improved term syntax

removed legacy proofs

spread NEWS about "induction_scheme" method

settings for cvs version of poly

tuned comments;

constructor: allow default logic; kill: refer to "isabelle.kill" system property;

constructor: allow default logic;

tuned whitespace;

compose command line according to isabelle.shell/home system properties;

tuned comments;

addClassPath;

added example session with Beanshell;

ExitThread: deliver message before EXIT;

tuned;

tuned;

* isatool browser now works with Cygwin; * isabelle-process: non-ML sessions are run with "nice"; * JVM class isabelle.IsabelleProcess (in Isabelle/lib/classes);

added javapath (for cygwin);

ExitThread: sleep(300) before delivering EXIT message;

reorganized demo;

reorganized demo;

class Result: replaced FAILURE by SYSTEM (internal notification); tuned isabelle command line -- explicit bash makes it work on cygwin also;

non-ML session: run with 'nice', to prevent isabelle process from flooding interactive front-ends (ProofGeneral/XEmacs etc.)

recover: not skip over "`";

package isabelle; replaced outputWrapped by outputSync;

text_of: made even more robust against recurrent errors; tuned;

added separate_chars;

removed unused escape_malformed;

outputWrapped: more robust initial synchronization;