1998-08-20 paulson 1998-08-20 Now qed_spec_mp respects locales, by calling ml_store_thm instead of bind_thm
1998-08-19 wenzelm 1998-08-19 fixed param;
1998-08-19 wenzelm 1998-08-19 assume: adjust_maxidx;
1998-08-19 paulson 1998-08-19 new version, more resistant to PROOF FAILED. Now it distinguishes between inferences that update the branch (resolve_tac) and those that do not (match_tac)
1998-08-19 paulson 1998-08-19 The warning "Rewrite rule from different theory" is ALWAYS printed, even if tracing is off.
1998-08-19 paulson 1998-08-19 new theorem zero_less_diff
1998-08-19 paulson 1998-08-19 Misc changes
1998-08-19 paulson 1998-08-19 Deleted obsolete declaration of PartE'
1998-08-19 paulson 1998-08-19 Tidied, removing uses of less_imp_diff_positive
1998-08-19 paulson 1998-08-19 tidied
1998-08-19 paulson 1998-08-19 fixed overloading of "image"
1998-08-19 paulson 1998-08-19 Overloading decl should assist Blast_tac
1998-08-19 paulson 1998-08-19 less_imp_diff_positive is redundant with new simprule zero_less_diff
1998-08-19 paulson 1998-08-19 Some new theorems. zero_less_diff replaces less_imp_diff_positive
1998-08-18 paulson 1998-08-18 ZF.thy
1998-08-18 paulson 1998-08-18 new theorem Un_Diff_Int
1998-08-18 paulson 1998-08-18 added comment
1998-08-18 paulson 1998-08-18 new theorem diff_Suc_less_diff
1998-08-17 wenzelm 1998-08-17 added get_tthmss;
1998-08-17 nipkow 1998-08-17 Mention RegExp2NA.
1998-08-17 paulson 1998-08-17 expandshort
1998-08-17 paulson 1998-08-17 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy contains fewer theorems than before
1998-08-17 paulson 1998-08-17 Now allows "." in rule names, with special treatment for "be"
1998-08-17 nipkow 1998-08-17 Direct translation RegExp -> NA!
1998-08-17 nipkow 1998-08-17 Additions to Lex.
1998-08-14 paulson 1998-08-14 got rid of some goal thy commands
1998-08-14 paulson 1998-08-14 now trans_tac is part of the claset...
1998-08-14 paulson 1998-08-14 Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML
1998-08-14 paulson 1998-08-14 expandshort
1998-08-14 paulson 1998-08-14 Uses Goal instead of "goal...thy" to avoid theory problems
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-08-13 paulson 1998-08-13 tidying
1998-08-13 paulson 1998-08-13 Moved the definition of s_u (as s) into the locale
1998-08-13 paulson 1998-08-13 Constrains, Stable, Invariant...more of the substitution axiom, but Union does not work well with them
1998-08-13 paulson 1998-08-13 simpler SELECT_GOAL no longer inserts a dummy parameter
1998-08-13 paulson 1998-08-13 Rule mk_triv_goal for making instances of triv_goal
1998-08-13 paulson 1998-08-13 Blast_tac is faster
1998-08-13 paulson 1998-08-13 stac now handles definitions as well as equalities
1998-08-13 paulson 1998-08-13 stac
1998-08-12 oheimb 1998-08-12 minor adaption for SML/NJ
1998-08-12 oheimb 1998-08-12 added theorems Id_o, o_Id corrected name of theorem: fund_upd_other -> fun_upd_other
1998-08-12 oheimb 1998-08-12 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
1998-08-12 oheimb 1998-08-12 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
1998-08-12 oheimb 1998-08-12 renamed mk_meta_eq to meta_eq
1998-08-12 oheimb 1998-08-12 removed superfluous o_apply
1998-08-12 oheimb 1998-08-12 streamlined proofs with new hoare_conseq1, hoare_conseq2
1998-08-12 oheimb 1998-08-12 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
1998-08-12 oheimb 1998-08-12 added Eps_eq
1998-08-12 oheimb 1998-08-12 removed use_thys implied by use_thy "Main"
1998-08-12 oheimb 1998-08-12 repaired proof of chfindom_monofun2cont
1998-08-12 oheimb 1998-08-12 added length_Suc_conv, finite_set
1998-08-12 oheimb 1998-08-12 replaced idt by pttrn in @filter
1998-08-12 oheimb 1998-08-12 replaced split_etas by split_eta_proc
1998-08-12 oheimb 1998-08-12 added ospec AddIffs [elem_o2s]
1998-08-12 oheimb 1998-08-12 minor correction: n must not be used as free variable
1998-08-12 slotosch 1998-08-12 eliminated fabs,fapp. changed all theorem names and functions into Rep_CFun, Abs_CFun
1998-08-10 wenzelm 1998-08-10 suffix, unsuffix moved to Pure/library.ML;
1998-08-10 wenzelm 1998-08-10 fixed comment;
1998-08-10 wenzelm 1998-08-10 tuned;
1998-08-10 wenzelm 1998-08-10 ??id syntax for text variables;