Now uses more carefully designed simpsets to prevent proofs from failing for some strange datatypes with nested recursion.

Test data generation and conversion to terms is now more closely intertwined, to allow displaying of functions in test data.

Eliminated DatatypeAux.dest_TFree to avoid clashes with Term.dest_TFree.

Added nil_const and cons_const.

Added test data generator for function type (from Pure/codegen.ML).

New interface for test data generators.

declare ch2ch_LAM [simp]

added overloading target

new compactness lemmas; removed duplicated flat_less_iff

Compactness subsection with new lemmas

Compactness subsection with some new lemmas

new compactness lemmas

new lemmas max_in_chainI, max_in_chainD

overloading target

tuned

added simp attributes/ proofs fixed

added simp attributes

Finally: no more unproven.

tuned

some more primrec

tuned

a note on syntax in class context

a note on syntax

tuned proofs

normalization conversion

tuned comment

explicit type variables for instantiation

better error reporting

tuned

refined overloading target

imp_conv_disj is now declared as a "code unfold" lemma to avoid that conclusion is evaluated eagerly.

isabelle.jars: temporarily disabled, until isatest gets up-to-date java;

some pre-release tunings

more robust console thread (cf. jedit plugin version);

build Isabelle process wrapper; build jEdit plugin, if Scala is available;

* Rudimentary Isabelle plugin for jEdit;

added plugin installation;

tuned;

purge build directory;

basic setup for Isabelle/jEdit plugin;

added interface for command-line option;

removed obsolete prompt and channel markups; replaced prompt markup by prompt channel setup (avoids left-over XML encoding); tuned;

replaced prompt markup by prompt channel setup;

removed obsolete prompt markup;

removed unused of_stream; tty: Output.prompt, avoid low-level TextIO;

added explicit prompt channel (prompt_fn/prompt); tuned;

removed obsolete prompt and channel markups;

Tuned relevant premises selection

tuned comments;

added symbol output mode, with XML escapes; improved message markup: get first position from body text; added INIT message, with pid and session property; removed adhoc PID handling; tuned;

export session id;

secure_main: removed separate welcome;

removed unused text_charref, cdata; added plain_content;

added INIT message, with pid and session property; removed adhoc PID handling;

more instantiation

adhering to instantiation policy

cleaned up some proofs

simplified some proofs

partially adapted to new inversion rules

adapted to new inversion rules

fixed typo

improved warning

add new is_ub lemmas; clean up directed_finite proofs

new instance proofs for classes finite_po, chfin, flat

new lemma flat_less_iff

generalized chfindom_monofun2cont

Implemented proof of strong case analysis rule.

Added function fresh_const.

Added function partition_rules'.

another attempt to disable documents;

simplified position_props, always include line/file fields;

replaced thread_properties by simplified version in position.ML;

nested_command: simplified properties vs. position -- the latter also includes id now;

type T: based on properties, added id field; added thread_data, setmp_thread_data (formerly in toplevel.ML); tuned signature;

moved id to position properties;

instance unit :: finite_po

new axclass finite_po < finite, po

add lub_maximal lemmas; modify conclusion of directed_finiteD; declare not_directed_empty [simp]

added class Property: basic Isabelle properties;

tuned relevance test for presburger

output message properties: id or position;

toplevel print_exn: proper setmp_thread_properties;

added id property;

Result: added props field; tuned;

remove legacy ML bindings

new-style theorem references

fix theorem references

generalized and simplified proof of adm_Finite

new lemma adm_upward

Tuned (type information in Lemmas)

Changed order of tactics in presburger --- thinning before case splits

maintain thread transition properties;

setmp_thread_data;

added setmp_thread_data;

type transition: added properties field;

added properties;

Isabelle.command: IsarCmd.nested_command (with properties);

added nested_command (with explicit position argument via properties);

of_properties: return filtered result;

added method encodeProperties; method command/ML: pass Properties; tuned error messages;

setting -H 2000 and no documents for higher performance;

add dcpo instance proof

declare upE as cases rule; add new rule up_induct

update sq_ord/po instance proofs

move lemmas from Cont.thy to Ffun.thy; reorder dependency of Cont.thy and Ffun.thy; add dcpo instance proofs for function type

remove not_up_less_UU [simp]

update instance proofs for sq_ord, po; new instance proofs for dcpo

add lemma ub2ub_monofun'

added dcpo instance proofs

new class dcpo; added dcpo versions of some lemmas

added new lemmas

add lemma dir2dir_monofun

tuned;

new is_ub lemmas; new lub syntax for set image

Multithreading.max_threads := 0 refers to number of cores of underlying machine;

added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;

added usedir -M max (alias for -M 0);

new section for directed sets

split of class uminus

empty dictionaries for OCaml