removed some legacy instantiations

improved evaluation mechanism

splitted class uminus from class minus

testing for empty sort

new metis proofs

renamed foldM to fold_mset on general request added Tobias' lemmas on fold_mset (A+B) etc tuned default simp set for fold_mset

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;

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;

Isar loop: recover after toplevel crashes;

secure_main: enforces terminator, to gain robustness;

text_of: make double sure that result is well-formed, to avoid recurrent failures;

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

added off-line parse; read: no recovery on non-interactive source, yields proper errors;

(alt)string: allow explicit character codes (as in ML);

added nested 'Isabelle.command';

updated;

special_end: replaced Z by dot;

output_prompt: CRITICAL;

declaration of instance parameter names

exported declare_names

new primrec

instantiation target rather than legacy instance

proper treatment of code theorems for primrec

dropped Instance.instantiate

Adding "ex/Induction_Scheme.thy" to tests

experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)

tuned further

renamed ML_PID to PID;

R&F: added sgn lemma Prefix: sledge-hammered

temporary code generator work arounds

fixed slip

-authentic primrec

dropped legacy bindings

authentic primrec

dropped void space

added new primrec package

load sum_tree.ML

factored out handling of sum types again

added test_markup; added channel markup and specials;

moved basic test_markup to isabelle_process.ML;

added channels; added markup operation, which operates on plain strings instead of raw output;

replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;

check persistent sessions;

tuned signature;

made SML/NJ happy;

removed -e flag from most sessions;

instance int,real :: lordered_ring

methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.

tuned class parts

dropped Classpackage.thy

tuned

added parser for multi_arity

added constrain_thm

canonical instantiation

map_product and fold_product

interface and distinct simproc tuned

improved

interpretation of typedefs

simplified infrastructure for code generator operational equality

added something about instantiation target

switch poly to 5.1, removed -e flag from most sessions

switch at-poly main to poly 5.1

make mac-poly non-experimental

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;