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]