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;
1998-04-04 wenzelm 1998-04-04 added triv_goal, rev_triv_goal (for Isar);
1998-04-04 wenzelm 1998-04-04 added Goal_def;
1998-04-04 wenzelm 1998-04-04 replaced thy_data by thy_setup;
1998-04-04 wenzelm 1998-04-04 added local_theory (for Isar); added setup;
1998-04-04 wenzelm 1998-04-04 tuned trace msgs;
1998-04-03 wenzelm 1998-04-03 tuned names;
1998-04-03 wenzelm 1998-04-03 added get_tthm(s), store_tthms(s); tuned;
1998-04-03 wenzelm 1998-04-03 tuned comments;
1998-04-03 wenzelm 1998-04-03 added attribute.ML;
1998-04-03 wenzelm 1998-04-03 Theorem tags and attributes.
1998-04-03 paulson 1998-04-03 UNITY
1998-04-03 oheimb 1998-04-03 repaired incompatibility with new SML version by eta-expansion
1998-04-03 paulson 1998-04-03 New target HOL-UNITY
1998-04-03 paulson 1998-04-03 New UNITY theory
1998-04-03 paulson 1998-04-03 Tidied proofs
1998-04-03 paulson 1998-04-03 Tidied proofs by getting rid of case_tac
1998-04-03 oheimb 1998-04-03 improved \tt appearance of many ASCII special symbols like # isabelle theory file keywords now appear bold only when at begin of line
1998-04-02 oheimb 1998-04-02 split_all_tac now fails if there is nothing to split split_all_tac has moved within claset() from usafe wrappers to safe wrappers
1998-04-02 paulson 1998-04-02 new theorems