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;