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;

help: unknown theory context;

added keep', theory';

help: unkown theory context;

ThmDatabase.print_thms_containing;

added print_thms_containing;

defs: axmdecl;

simplified sectioned_args;

added reset_thms; add_binds(_i): admit unbinding;

added reset_thms; prep_result: check prop;

tuned;

defs: name mandatory;

avoid interrupts of read loop;

simplified sectioned_args; tuned;

Proof.reset_thms calculationN;

admit unbinding;

unfold / fold defs;

skolem_tag;

added fold_rule;

* HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar) -- by Gertrud Bauer;

working version with co-guarantees-leadsto results

tuned;

tuned;

qed "";

tuned print_result;

improved cycle error;

Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or RealAbs. RealAbs proofs have been highly streamlined. A couple of RealPow proofs use #1, #2, etc.

sep1 -> sep

The restrict_to_left rule fixes some bugs

Sets new component "restrict_to_left"

tidied; added lemma restrict_to_left

Restructured lin.arith.package and fixed a proof in RComplete.

Restructured lin.arith.package.

thms_containing: single writeln;

tuned pretty_thms;

added thms_containing;

qed "";

proper theory setup for Real/ex/BinEx;

tuned;

improved output;

added 'insert' method (again);

ml_store_thm: no warning for "";

present results;

merged in lost update;

Mod because of new solver interface.

?

Solvers are now named and stamped.

fixed unfold of facts;

accomodate refined facts handling;

accomodate refined facts handling; tuned;

Main;

Thm.no_prems;