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;

tuned;

added some ~= rules;

removed "case" thm;

setup for refined facts handling; Method.bang_sectioned_args / Args.bang_facts;

setup for refined facts handling; Method.bang_sectioned_args / Args.bang_facts; eliminated asm_simp; tuned improper methods;

export prems_of;

setup_goal: do not insert assumptions;

setup for refined facts handling; tuned insert_facts, assumption, (un)fold; insert_tac: no rotate_tac, order was OK in the first place; added ctxt_args, bang_sectioned_args; added assm_tac;

differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);

added bang_facts;

Added comments.

Now distinguishes discrete from non-distrete types.

moved inf_of(?) to hologic.

Integ/bin_simprocs.ML now loaded in Integ/Bin.ML

ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML

new proof of drop_prog_correct for new definition of project_act

project_act no longer has a special case to allow identity actions

fixed SOUNDNESS BUG concerning the map from terms like ?f x y to SVC variables

Fixed bug in add_primrec which caused non-informative error message.

renamed Always_Int to Always_Int_I

new theorem mono_Follows_apply

new theorem Always_INT_distrib; therefore renamed Always_Int to Always_Int_I

working Safety proof for the system at last

now uses Pattern.aeconv, not aconv, to test equality between the terms abstracted over; otherwise it is incomplete. Other changes are cosmetic

new rule PLam_ensures

working snapshot

new theorem image_image_eq_UN

The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) (by Gertrud Bauer, TU Munich);

added no_prems;

minor change to smp_tac

fixed url;

AddXDs [bspec];

tuned;

AddXIs [disjI1, disjI2];

removed obsolete comment;

lemma less_add;

(un)fold: ignore facts;

more rational theorem names (?)

tidied

more rational theorem names (?)

ensures_tac now handles leadsTo as well as LeadsTo

new theorem single_Diff_lessThan

now uses the identity function

simplification of relations involving 0, Suc and natural-number numerals

generalized the theorem zless_zero_nat to zless_nat_eq_int_zless, and reorganized

generalized the theorem bin_add_BIT_Min to bin_add_Min_right

moved identity theorems to Fun.ML

comments

images and preimages of the identity function

new example HOL/UNITY/TimerArray

rule option;

\indexisarmeth: "Methods";

tuned (then_)apply;

url;

\url;

induct method: rule option;

Method.refine_no_facts;

read_def_termT: dummyT;

then_tac = refine;

read_typ/term: context_of;

tuned;

added context_of;

logtypes: pretend "dummy" is one;

isatool expandshort;

expandshort usage: forward_tac;

strengthened card_seteq

added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD

added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc

added theorems le_maxI1 and le_maxI2, also in claset

added theorem dvd_reduce

*** empty log message ***

added ftac, eatac, datac, fatac

added smp_tac

added;

isabelle-pdfdocs;

close_block: removed ProofContext.transfer_used_names;

removed thms_closure (unused); removed transfer_used_names; fix: do not declare unconstrained vars;

removed thms_closure (unused);

added README;

tuned;

working snapshot

goal_nonempty: Ex goal for new-style version;

replaced ?? by ?;

eliminated Syntax.binding; put_thms: ignore ""; update_binds_env: Envir.norm_term ensures proper type instantiation;

deactivated ProofContext.transfer_used_names; eliminated PureThy.default_name ("" not stored);

removed text vars;

PureThy.have_thmss: "" replaces None;

Library.equal_lists;

removed Syntax.binding;

removed "_BIND" translation;

removed binding;

removed "_BIND" syntax;

eliminated default_name (thms no longer stored for name "");

ProtoPure: fake empty scope;

equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool;