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;
1998-08-10 wenzelm 1998-08-10 dest_binding, dest_skolem;
1998-08-10 wenzelm 1998-08-10 val single: 'a -> 'a list; val suffix: string -> string -> string; val unsuffix: string -> string -> string;
1998-08-10 paulson 1998-08-10 Tidying of AC, especially of AC16_WO4 using a locale
1998-08-10 nipkow 1998-08-10 More lemmas about lex.
1998-08-08 nipkow 1998-08-08 *** empty log message ***
1998-08-08 nipkow 1998-08-08 List now contains some lexicographic orderings.
1998-08-06 wenzelm 1998-08-06 added store_tthm;
1998-08-06 berghofe 1998-08-06 Improved well-formedness check.
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-08-06 paulson 1998-08-06 A higher-level treatment of LeadsTo, minimizing use of "reachable"
1998-08-06 nipkow 1998-08-06 Simplified proof!!
1998-08-06 nipkow 1998-08-06 *** empty log message ***
1998-08-06 nipkow 1998-08-06 Lemma renamed in HOL.
1998-08-06 nipkow 1998-08-06 Added macro `termi'
1998-08-06 nipkow 1998-08-06 New lemmas in List and Lambda in IsaMakefile
1998-08-06 nipkow 1998-08-06 Removed duplicate thms (see comment to Arith.ML)
1998-08-06 nipkow 1998-08-06 Removed duplicate thms: less_imp_add_less = trans_less_add1 le_imp_add_le = trans_le_add1
1998-08-06 nipkow 1998-08-06 Removed comments.
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-08-06 paulson 1998-08-06 disjointness
1998-08-06 paulson 1998-08-06 Now recognizes both {}= and ={}
1998-08-06 paulson 1998-08-06 Disjointness reasoning by AddEs [equals0E, sym RS equals0E] and consequential changes (and tidying)
1998-08-06 paulson 1998-08-06 New result from AC directory
1998-08-06 wenzelm 1998-08-06 added solve_tac;
1998-08-06 paulson 1998-08-06 New results from AC
1998-08-06 nipkow 1998-08-06 First steps towards termination of simply typed terms.
1998-08-06 wenzelm 1998-08-06 binding / skolem vars;
1998-08-05 paulson 1998-08-05 Null program and a few new results
1998-08-05 paulson 1998-08-05 Finished the example
1998-08-05 paulson 1998-08-05 Indentation, comments
1998-08-05 paulson 1998-08-05 Renamed equals0D to equals0E
1998-08-05 paulson 1998-08-05 Tidied
1998-08-05 paulson 1998-08-05 Removal of "disjoint" translation
1998-08-05 paulson 1998-08-05 New record type of programs
1998-08-05 paulson 1998-08-05 Union primitives and examples
1998-08-04 wenzelm 1998-08-04 tuned; Display.print_goals function moved to Locale.print_goals;
1998-08-04 wenzelm 1998-08-04 added LocaleGroup, PiSets examples;
1998-08-04 wenzelm 1998-08-04 added Open_locale, Close_locale; thm(s): use Locale.get_thm(s);
1998-08-04 wenzelm 1998-08-04 added 'locale' section;
1998-08-04 wenzelm 1998-08-04 Locale.setup;
1998-08-04 wenzelm 1998-08-04 added export: thm -> thm; exported print_current_goals_default; locale support;