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;

Result: added STDOUT, SIGNAL; renamed method destroy to kill; method kill: close--sleep--destroy; tuned;

option -m: avoid additional quoting;

tuned whitespace;

proper termination of stdout thread; tuned;

added exit thread; added destroy method; tuned;

tuned diagnostics;

run Isabelle process with plain tty interaction;

added output protocol specification; PID: always on new line;

tuned;

added isatool tty;

added ISABELLE_LINE_EDITOR setting;

added ISABELLE_LINE_EDITOR; tuned;

* isatool tty runs Isabelle process with plain tty interaction;

nested commands: avoid nested errors;

added close_witness;

removed syntax in locale left_commutative

changed order in class parameters

heutistics for type annotations in Haskell

simplified

memorizing and exporting destruction rules

improved rule calculation

exported axiomsN

added div/mod examples

target language div and mod

clarified heading

dropped ws

added lemma

isatool codegen now returns exit value

a fold operation for multisets + more lemmas

tuned

adjusted

pretty for instantiation and overloading

continued

error handling for pathological cases

dropped induction rule

dropped Class.prep_spec

moved lemma odd_pos to theory Parity

joined StarClasses theory with StarDef

joined EvenOdd theory with Parity

tuned

added simple primitive note

moved instance parameter management from class.ML to axclass.ML

tuned header

switched import from Main to List

switched import from Main to PreList

explicit import of theory ATP_Linkup

explicit import of theory Main

swtiched ATP_Linkup and PreList in theory hierarchy

ML_OPTIONS="-H 1500" -- potentially works around GC core dump;

added Id, some cleanup

tuned message;

renamed IsabelleResult to IsabelleProcess.Result;

Isabelle process wrapper for JVM platform (tentative implementation in Java, which is to be replaced by a sane source language eventually);

tuned messages;