tidying

Moved the definition of s_u (as s) into the locale

Constrains, Stable, Invariant...more of the substitution axiom, but Union does not work well with them

simpler SELECT_GOAL no longer inserts a dummy parameter

Rule mk_triv_goal for making instances of triv_goal

Blast_tac is faster

stac now handles definitions as well as equalities

stac

minor adaption for SML/NJ

added theorems Id_o, o_Id corrected name of theorem: fund_upd_other -> fun_upd_other

cleanup for Fun.thy: merged Update.{thy|ML} into Fun.{thy|ML} moved o_def from HOL.thy to Fun.thy added Id_def to Fun.thy moved image_compose from Set.ML to Fun.ML moved o_apply and o_assoc from simpdata.ML to Fun.ML moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML added fun_upd_twist to Fun.ML

the splitter is now defined as a functor moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML moved split_thm_info to Provers/splitter.ML definined atomize via general mk_atomize removed superfluous rot_eq_tac from simplifier.ML HOL/simpdata.ML: renamed mk_meta_eq to meta_eq, re-renamed mk_meta_eq_simp to mk_meta_eq added Eps_eq to simpset

renamed mk_meta_eq to meta_eq

removed superfluous o_apply

streamlined proofs with new hoare_conseq1, hoare_conseq2

defined map_upd by translation via fun_upd changed syntax of map_upd to be consistent with that of fun_upd added chg_map, map_upds

added Eps_eq

removed use_thys implied by use_thy "Main"

repaired proof of chfindom_monofun2cont

added length_Suc_conv, finite_set

replaced idt by pttrn in @filter

replaced split_etas by split_eta_proc

added ospec AddIffs [elem_o2s]

minor correction: n must not be used as free variable

eliminated fabs,fapp. changed all theorem names and functions into Rep_CFun, Abs_CFun

suffix, unsuffix moved to Pure/library.ML;

fixed comment;

tuned;

??id syntax for text variables;

dest_binding, dest_skolem;