New target HOL-UNITY

New UNITY theory

Tidied proofs

Tidied proofs by getting rid of case_tac

improved \tt appearance of many ASCII special symbols like # isabelle theory file keywords now appear bold only when at begin of line

split_all_tac now fails if there is nothing to split split_all_tac has moved within claset() from usafe wrappers to safe wrappers

new theorems

changed if_bool_eq to if_bool_eq_conj

changed if_bool_eq to if_bool_eq_conj and added if_bool_eq_disj

New theorems card_Diff_le and card_insert_le; tidied

introduced functions for updating the wrapper lists merge_cs now uses merge_alists to merge wrapper lists, left cs has precedence!

*** empty log message ***

merge_cs now also merges safe and unsafe wrappers

generalized appearance of trancl_into_rtrancl and r_into_trancl added irrefl_tranclI, reflcl_trancl, trancl_reflcl, trancl_empty, rtrancl_empty

adapted proof of finite_converse

added wf_converse_trancl, adapted proof of wfrec

added caveat

added introduction and elimination rules for Univalent

added Univalent_rel_pow

removed superfluous use_thy

removed superfluous translations

added try, single, many; improved source: prompt;

added cproj', and therefore extended prj tried to fix polymorphism problem for take_defs. A full solution will require significant changes.

added cproj', and therefore extended prj

improved checks

added o2s

added finite_acyclic_wf_converse: corrected 8bit chars

added acyclicI

added finite_acyclic_wf_converse

more thms

inverse -> converse

inverse -> converse [It is standard terminology and also used in ZF]

re-ordered proofs

moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;

renamed not1_or to disj_not1, not2_or to disj_not2

improved coding of delWrapper and delSWrapper

addloop: added warning in case of overwriting a looper

Made mutual simplification of prems a special case.

Used merge_alists for loopers.

New, stronger rewrites

The theorem nat_neqE, and some tidying

New laws, mostly generalizing old "pred" ones

spy_analz_tac now handles individual conjuncts properly

new theorem

New theorem Image_eq_UN; deleted the silly vimage_inverse_Image

Arith.thy -> thy; proved a few new theorems

New Asm_full_simp_tac shortens proof.

Simplifier

More Lex.

New Asm_full_simp_tac led to a loop.

Mod because of new simplifier.

Mod because of not1_or.

Updated proofs because of new simplifier.

Updated proofs because of new simplification tactics.

Adapted proofs because of new simplification tactics.

The new asm_lr_simp_tac is the old asm_full_simp_tac. The new asm_full_simp_tac also does a limited amount of mutual simplification.

renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin

added not1_or and if_eq_cancel to simpset() renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin

added not1_or and if_eq_cancel to simpset()

new rewrite rules not1_or, not2_or, and if_eq_cancel added not1_or and if_eq_cancel to simpset()

renamed smart_tac to force_tac, slight improvement of force_tac

Asm_full_simp_tac now reorients asm c = t to t = c.

adhoc fix of is_blank;

New scanner in abstract form.

New simplifier flag for mutual simplification.

Removed expand_split from simpset.

removed pred;

eliminated pred function;

Symbol.explode;

replaced $LOGNAME by $USER;

tuned;

Symbol.is_*;

adapted to new scanner, baroque chars;

Symbol.input;

adapted to symbols, scan;

Generic scanners (for potentially infinite input) -- replaces Scanner;

adapted to new scanner and abroque chars;

read_var;

Symbol.output;

tuned syntax error msg;

Symbol.explode;

scan.ML, symbol.ML;

adapted to new scanners and baroque chars;

tuned some names;

adapted to baroque chars;

added merge_alists; moced is_letter etc. to Syntax/symbol.ML;

Syntax.indexname;

tuned comment;

tuned;

replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML; added Pure/Syntax/scan.ML;

replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;

Removed `addsplits [expand_if]'

added clasimp.ML;

Removed superfluous `op'

*** empty log message ***

Added delspilts, Addsplits, Delsplits.

expand_if is now by default part of the simpset.

New theorem and simprules

Reorganized simplifier. May now reorient rules. Moved loop tests from logic to thm.

Reorganized simplifier. May now reorient rules. This breaks many of the proofs in this file. Deactivated the feature locally.

Reorganized simplifier. May now reorient rules.

Better simplification allows deletion of parts of proofs

New theorem

New theorems

New theorems; tidied

New theorem diff_Suc_le_Suc_diff; tidied another proof

auto generated

Modified def.

Splitters via named loopers.

Little reorganization. Loop tactics have names now.

Tried to reorganize rewriter a little. More to be done.

added minimal description of rep_cs: corrections

added minimal description of rep_cs

added minimal description of rep_ss

"choice" moved to Set.ML

New absorbsion laws, etc

Vimage

New vimage laws

added smart_tac

removed superfluous addss

New theory, Vimage

Proved choice and bchoice; changed Fun.thy -> thy

*** empty log message ***

added clasimp.ML;

renamed rep_claset to rep_cs

factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML explicitly introducing combined type clasimpset

changed wrapper mechanism of classical reasoner

added split_all_tac to claset()

changed wrapper mechanism of classical reasoner

New theory of the inverse image of a function

Added some lemmas.

Catches bad elim rules, handling exception OPTION

New laws for union

New laws for id

New induction schemas for lists (length and snoc).

*** empty log message ***

Congruence rules use == in premises now.

Congruence rules use == in premises now. New class linord.

minor improvements

re-arranged bindings for many function keys

extended input syntax to handle names of special keys

moved Ctrl entry before Alt entry extended input syntax to handle names of special keys

New theorem eq_imp_le

Four new Union/Intersection laws

corrected problem with auto_tac: now uses a variant of depth_tac that avoids interference of the simplifier with dup_step_tac

added New Jersey mirror;

Improved loop-test for rewrite rules a little. Should be done properly!

tuned comment;

added append (curried);

*** empty log message ***

Sign.merge vs. Sign.nontriv_merge;

tuned comments;

oops;

tuned print_cs;

updated;

tuned;

added explicit signature; improved comments;

improved comments;

fixed add_trrules: intern root;

export map_trrule;

tuned add_trrules;

improved is_letter etc.;

New Addsimps for Compl rules

New AddIffs le_0_eq and neq0_conv

Replaced ALLNEWSUBGOALS by THEN_ALL_NEW

Used THEN_ALL_NEW.

moved freeze_thaw to drule.ML

Tidying; rotate_prems; moved freeze_thaw from tactic.ML

AC and other rewrite rules for Un and Int

auto update

Added reference to rotate_prems

filter_size -> length_filter

Added `remdups' nodup -> nodups

added Vartab: TABLE;

added param;

added THEN_ALL_NEW;

New theorem Image_id

New theorem order_eq_refl

New max, min theorems

Added some more explicit guarantees of key secrecy for agents Deleted spurious A~=Spy assumptions

Fixed a lot of overfull and underfull lines (hboxes)

Updated the description of how to set up hyp_subst_tac

New example, Pow_Sigma_bij

fixed WWW links

Three new facts about Image

Replaced \\1 by $1 as Perl itself asked me to...

Fixed the description of recdef

tuned msgs;

improved tracing of rewrite rule application;

removed dead messy code;

added read_var;

tuned;