1998-04-29 wenzelm 1998-04-29 tuned error msgs;
1998-04-29 wenzelm 1998-04-29 moved mk_defpair to logic.ML; moved get_def to thm.ML; moved require_thy to theory.ML;
1998-04-29 wenzelm 1998-04-29 tuned get_ax (uses ancestry); added get_def: theory -> xstring -> thm;
1998-04-29 wenzelm 1998-04-29 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);
1998-04-29 wenzelm 1998-04-29 adapted to new PureThy.add_axioms_i;
1998-04-29 wenzelm 1998-04-29 added defaultS: sg -> sort; added full_name_path: sg -> string -> bstring -> string; added add_nonterminals: bstring list -> sg -> sg;
1998-04-29 wenzelm 1998-04-29 added thm, thms;
1998-04-29 wenzelm 1998-04-29 *** empty log message ***
1998-04-28 paulson 1998-04-28 new thms, really demos of the final coalgebra theorem
1998-04-28 paulson 1998-04-28 new thms image_0_left, image_Un_left, etc.
1998-04-28 paulson 1998-04-28 new thm mult_lt_mono1
1998-04-27 oheimb 1998-04-27 cleanup for split_all_tac as wrapper in claset()
1998-04-27 oheimb 1998-04-27 removed wrong comment
1998-04-27 oheimb 1998-04-27 added option_map_eq_Some via AddIffs
1998-04-27 nipkow 1998-04-27 *** empty log message ***
1998-04-27 nipkow 1998-04-27 delsplits, Addsplits, Delsplits.
1998-04-27 nipkow 1998-04-27 Renamed expand_const -> split_const
1998-04-27 nipkow 1998-04-27 Added conversion of reg.expr. to automata. Renamed expand_const -> split_const.
1998-04-27 nipkow 1998-04-27 Renamed expand_const -> split_const.
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-04-27 paulson 1998-04-27 New proof of apply_equality and new thm Pi_image_cons
1998-04-24 oheimb 1998-04-24 improved split_all_tac significantly
1998-04-24 oheimb 1998-04-24 improved keyboard modifiers
1998-04-24 oheimb 1998-04-24 added ASCII translation of subseteq
1998-04-24 paulson 1998-04-24 tidied; div & mod
1998-04-24 oheimb 1998-04-24 *** empty log message ***
1998-04-22 wenzelm 1998-04-22 added no_syn;
1998-04-22 wenzelm 1998-04-22 added mk_cond_defpair, mk_defpair;
1998-04-22 nipkow 1998-04-22 Modifications due to improved simplifier.
1998-04-22 nipkow 1998-04-22 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.
1998-04-21 oheimb 1998-04-21 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
1998-04-21 oheimb 1998-04-21 split_all_tac is now added to claset() _before_ other safe tactics
1998-04-21 oheimb 1998-04-21 made proof of zmult_congruent2 more stable
1998-04-21 oheimb 1998-04-21 simplification of explicit theory usage and merges
1998-04-21 oheimb 1998-04-21 removed split_all_tac from claset() globally within IOA
1998-04-21 oheimb 1998-04-21 made modifications of the simpset() local significantly simplified (and stabilized) proof of is_asig_of_rename
1998-04-21 oheimb 1998-04-21 layout improvement
1998-04-21 paulson 1998-04-21 expandshort; new gcd_induct with inbuilt case analysis
1998-04-21 paulson 1998-04-21 Renamed mod_XXX_cancel to mod_XXX_self Included their div_ equivalents
1998-04-20 paulson 1998-04-20 New laws for mod
1998-04-20 paulson 1998-04-20 proving fib(gcd(m,n)) = gcd(fib m, fib n)
1998-04-19 wenzelm 1998-04-19 fixed comment;
1998-04-10 paulson 1998-04-10 Fixed bug in inductive sections to allow disjunctive premises; added tracing flag trace_induct
1998-04-10 paulson 1998-04-10 bug fixes
1998-04-10 paulson 1998-04-10 can prove the empty relation to be WF
1998-04-10 paulson 1998-04-10 Fixed bug in inductive sections to allow disjunctive premises; added tracing flag trace_induct
1998-04-09 paulson 1998-04-09 Clearer description of recdef, including use of {}
1998-04-09 paulson 1998-04-09 Simplified the syntax description; mentioned FOL vs HOL
1998-04-07 oheimb 1998-04-07 *** empty log message ***
1998-04-07 oheimb 1998-04-07 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()
1998-04-07 oheimb 1998-04-07 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.
1998-04-04 wenzelm 1998-04-04 no open Simplifier;
1998-04-04 wenzelm 1998-04-04 tuned fail;
1998-04-04 wenzelm 1998-04-04 type_error; replaced thy_data by setup;
1998-04-04 wenzelm 1998-04-04 tuned comments; BasicSimplifier made pervasive; added simp tags / attributes; replaced thy_data by setup;
1998-04-04 wenzelm 1998-04-04 no open Simplifier;
1998-04-04 wenzelm 1998-04-04 replaced thy_data by thy_setup;
1998-04-04 wenzelm 1998-04-04 type_error;
1998-04-04 wenzelm 1998-04-04 replaced thy_data by setup;
1998-04-04 wenzelm 1998-04-04 removed simple; added fail, untag;