system;

markup / varbatim: comment out (%) newline char;

use_text writeln;

mkdir, copy_all: system_command;

updated;

Eliminated mutual_induct_tac.

Eliminated mutual_induct_tac.

Eliminated mutual_induct_tac.

more Collect laws

deleted the redundant less_imp_binomial_eq_0

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;

$ISATOOL;

unset ISABELLE_SETTINGS_PRESENT;

delete Tools;

Documented changes to HOL/inductive and function thm_deps.

Added file Thy/thm_deps.ML

obsolete;

tuned dirname;

removed TeX environment hacking;

verbatim / verb markupup commands;

Present.token_source after load (better errors!?);

Document preparation setup;

Isabelle wrapper for LaTeX (and friends);

verbatim: no markup;

ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;

tex_source: Buffer.write;

present source *before* theory load;

removed write_nonempty;

New option -d for deleting file after use.

New function thm_deps for visualizing dependencies of theorems.

Added file thm_deps.

Exported function get_info.

ISABELLE_USEDIR_OPTIONS: -d pdf option (off by default);

improved presentation;

Isar_examples/W_correct;

tuned presentation;

tuned markup commands;

Latex.token;

improved presentation;

improved present_token;

added write_nonempty;

fixed naming of single axioms;

accomodate markup commands;

tuned comment;

added markup_command;

OuterSyntax.markup_command;

improved presentation;

added document;

simplified; header command;

strip_blanks;

got rid of most;

rep_datatype now stores theorems properly.

fixed title;

added document;

tuned comments;

tuned comment;

fixed ml_store_thm(s): deriv;

document preparation options: -c -d;

conditional url/hyperref setup;

present token source;

replace add_title by add_header;

clear_undo replaced by clear_undos; title replaced by header;

added is_toplevel;

clear: int argument;

use_dir: doc;

replaced clear_undo by clear_undos;

outer_lex.ML loaded in Thy;

include browser_info stuff; tex source presentation;

Simple LaTeX presentation primitives (based on outer lexical syntax).

begin_index: document; verbatim_source;

moved stuff to present.ML;

added Thy/latex.ML; removed Thy/browser_info.ML; use "../Isar/outer_lex.ML";

Got rid of readtm.

Tuned inductive definition.

updated;

added Thy/latex.ML; removed Thy/browser_info.ML (stuff now in Thy/present.ML);

Present.setup;

Added attribute rulify_prems (useful for modifying premises of introduction rules of inductive sets).

added copy_all; removed source;

clear: int arg;

added position;

Additional rules for inductive package.

added untabify;

Rule not_not is now stored in theory (needed by Inductive).

Monotonicity rules for inductive definitions can now be added to a theory via attribute "mono".

macros for Isabelle generated LaTeX output;

arithmetic now in IntArith;

simprocs now in IntArith;

IntArith;

Tools/typedef_package.ML;

eliminated ap/app;

proper dependencies of all theories and packages;

removed DatatypePackage.setup;

load / setup recdef package (TFL);

load / setup datatype package;

removed TFL/sys.sml; removed Integ/simproc.ML, Integ/bin_simprocs.ML; added Integ/IntArith.ML, Integ/IntArith.thy;

obsolete;

renamed 'prefix' to 'prfx' (avoids clash with infix);

tuned;

mk_frees, assume_read moved here; FOLogic.mk_conj, FOLogic.mk_disj;

tryres, gen_make_elim moved here;

FOLogic.mk_conj;

added mk_conj, mk_disj, mk_imp;

added BVC;

added mk_conj, mk_disj, mk_imp;

working snapshot (even Alloc)

most results now refer to those for "extend"

fixed lookup_theory;

fixed CHANGED_GOAL, which is used by stac

improved theory_source presentation (hook);

improved theory_source presentation;

export token_source; improved Present.theory_source;

added Space, Comment token kinds (keep actual text); source: do not filter proper;

fixed no_qed;

added Isar/obtain.ML;

improved 'fix' / Skolem interfaces;

added 'obtain' command;

tuned comment;

added prf_asm_goal;

added atomic_thesis;

The 'obtain' language element -- achieves (eliminated) existential quantification proof command level.

added undef_global_attribute, undef_local_attribute;

- Fixed bug in mk_split_pack which caused application of expansion theorem to fail because of typing reasons - Rewrote inst_lift and inst_split: now cterm_instantiate is used to instantiate theorems

fixed 'is' match;

added cert_skolem; removed declare_thm; context: removed maxidx; added maxidx_of_pair for proper unification;

export find_free;

removed ProofContext.declare_thm;

local_def_i: typ option; admit additional (fixed) type vars on rhs;

fix_i, local_def_i: typ option;

get_goal: prop; fix_i: typ option;

insert: ignore facts;

export def_sort, def_type; fix_i: typ option; init: maxidx = 0 is workaround for obscure bug in Unify.smash_unifiers;

Real/HahnBanach;

depend on Main;

now with (weak safety) guarantees (weak progress) with Extend

bind_thm ("case_split", case_split_thm);

CollectE; AddXIs [subsetD, rev_subsetD, psubsetI];

subsetD;

update from Gertrud;

The Hahn-Banach theorem for real vectorspaces;

bind_thms;

Sign.defaultS;

Sign.of_sort;

tuned;

removed force_strip_shyps;

lemma;

bind_thms;

proper handling of dangling sort hypotheses (at last!);

mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes (asm_simp performance!);

Sign.defaultS;

strip_shyps(_warning);

mg_domain: exception DOMAIN; proper witness_sorts; removed nonempty_sort;

removed implies_intr_shyps; removed force_strip_shyps (at last!); strip_shyps: proper witness_sorts; fix_shyps: tuned for all_sorts_nonempty;

added witness_sorts, univ_witness; removed nonempty_sort; tsig: log_types, univ_witness (require rebuild_tsig!); heavily tuned;

added witness_sorts, univ_witness; removed nonempty_sort;

handle Sorts.DOMAIN;

added rems_sort;

use Drule.strip_shyps_warning; removed Thm.implies_intr_shyps;

strip_shyps_warning;

new tsig components;

more sections;

present sections;

removed extra shyps error;

added string_of: text -> string;

working snapshot with new theory "Project"

tuned;

tidied, using "warning" function and fixing the Close_locale bug

added BCV.

A new theory: a model of bytecode verification.

zero_is_mult, by symmetry

new UNITY theory: Project

AC rules for equality

zero_is_mult, by symmetry

added W_correct -- correctness of Milner's type inference algorithm W (let-free version);

documented type solver

incompatibility solver

more tidying

removed order-sorted theorems from the default claset

added 'thms_containing', 'ML_setup';

added print_thms_containing; use_mltext: strictly diag;

use_mltext: Context.setmp only; use_mltext(_theory): verbose if int;