moved mk_defpair to logic.ML; moved get_def to thm.ML; moved require_thy to theory.ML;

tuned get_ax (uses ancestry); added get_def: theory -> xstring -> thm;

renamed setup to apply; added add_nonterminals: bstring list -> theory -> theory; added parent_path: theory -> theory; added root_path: theory -> theory; added require: theory -> string -> string -> unit (from section_utils.ML);

adapted to new PureThy.add_axioms_i;

added defaultS: sg -> sort; added full_name_path: sg -> string -> bstring -> string; added add_nonterminals: bstring list -> sg -> sg;

added thm, thms;

*** empty log message ***

new thms, really demos of the final coalgebra theorem

new thms image_0_left, image_Un_left, etc.

new thm mult_lt_mono1

cleanup for split_all_tac as wrapper in claset()

removed wrong comment

added option_map_eq_Some via AddIffs

*** empty log message ***

delsplits, Addsplits, Delsplits.

Renamed expand_const -> split_const

Added conversion of reg.expr. to automata. Renamed expand_const -> split_const.

Renamed expand_const -> split_const.

Added a few lemmas. Renamed expand_const -> split_const.

New proof of apply_equality and new thm Pi_image_cons

improved split_all_tac significantly

improved keyboard modifiers

added ASCII translation of subseteq

tidied; div & mod

*** empty log message ***

added no_syn;

added mk_cond_defpair, mk_defpair;

Modifications due to improved simplifier.

Tried to speed up the rewriter by eta-contracting all patterns beforehand and by classifying each pattern as to whether it allows first-order matching.

improved pair_tac to call prune_params_tac afterwards improved the (bad) efficiency of split_all_tac by about 50% split_all_tac is now added to claset() _before_ other safe tactics

split_all_tac is now added to claset() _before_ other safe tactics

made proof of zmult_congruent2 more stable

simplification of explicit theory usage and merges

removed split_all_tac from claset() globally within IOA

made modifications of the simpset() local significantly simplified (and stabilized) proof of is_asig_of_rename

layout improvement

expandshort; new gcd_induct with inbuilt case analysis

Renamed mod_XXX_cancel to mod_XXX_self Included their div_ equivalents

New laws for mod

proving fib(gcd(m,n)) = gcd(fib m, fib n)

fixed comment;

Fixed bug in inductive sections to allow disjunctive premises; added tracing flag trace_induct

bug fixes

can prove the empty relation to be WF

Fixed bug in inductive sections to allow disjunctive premises; added tracing flag trace_induct

Clearer description of recdef, including use of {}

Simplified the syntax description; mentioned FOL vs HOL

*** empty log message ***

replaced option_map_SomeD by option_map_eq_Some (RS iffD1) added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset()

made split_all_tac as safe wrapper more defensive: if it is added as unsafe wrapper again (as its was before), this does not break the current proofs.

no open Simplifier;

tuned fail;

type_error; replaced thy_data by setup;

tuned comments; BasicSimplifier made pervasive; added simp tags / attributes; replaced thy_data by setup;

no open Simplifier;

replaced thy_data by thy_setup;

type_error;

replaced thy_data by setup;

removed simple; added fail, untag;

added triv_goal, rev_triv_goal (for Isar);

added Goal_def;

replaced thy_data by thy_setup;

added local_theory (for Isar); added setup;

tuned trace msgs;

tuned names;

added get_tthm(s), store_tthms(s); tuned;

tuned comments;

added attribute.ML;

Theorem tags and attributes.

UNITY

repaired incompatibility with new SML version by eta-expansion

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.