choose just as an infix

simplified and generalized n_sub_lemma and n_subsets

working snapshot; more steps in Alloc

projecting/extending version of drop_prog_guarantees

new theorem set_mono

a4paper;

a4paper;

a4paper; tuned;

a4paper;

new "choose" lemmas by Florian Kammueller

improved presentation;

bind_thm "ccontr";

files: separate by " ";

- Documented monotonicity theorems. - Tuned accessible part example.

a4paper;

tuned packages;

a4paper;

working shapshot with "projecting" and "extending"

replaced {x. True} by UNIV to work with the new simprule, Collect_const

new default simprule Collect_const and new them Diff_insert_absorb

new thm vimage_INT; deleted redundant UN_vimage

new thm Domain_mono

new thm card_Diff_singleton; tidied

more explanations;

tuned presentation;

added structured version of the proof;

improved;

bib;

support bibtex; tuned;

check format; support bibtex;

added ISABELLE_BIBTEX;

removed 8bit;

\isakeyword: italic correction;

old_header: proper error message;

tuned presentation;

update from Gertrud;

tuned;

url;

theorem database now also indexes constants "Trueprop", "all", "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;

improved;

removed generated index.html;

isatool_document;

make: tuned usage;

improved presentation;

include document;

return stored thms with proper naming in derivation;

improved special chars;

removed -c option;

tuned usage;

pass RC;

prepare theory session document;

*** empty log message ***

tuned;

cd: quiet;

verbatim markup tokens;

removed verbatim markups;

unset ISABELLE_SETTINGS_PRESENT;

Replaced update_new by update.

Added functions for enabling and disabling derivations.

read_idents;