1998-03-09 wenzelm 1998-03-09 adapted to baroque chars;
1998-03-09 wenzelm 1998-03-09 added merge_alists; moced is_letter etc. to Syntax/symbol.ML;
1998-03-09 wenzelm 1998-03-09 Syntax.indexname;
1998-03-09 wenzelm 1998-03-09 tuned comment;
1998-03-09 wenzelm 1998-03-09 tuned;
1998-03-09 wenzelm 1998-03-09 replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML; added Pure/Syntax/scan.ML;
1998-03-09 wenzelm 1998-03-09 replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1998-03-06 wenzelm 1998-03-06 added clasimp.ML;
1998-03-06 nipkow 1998-03-06 Removed superfluous `op'
1998-03-06 nipkow 1998-03-06 *** empty log message ***
1998-03-06 nipkow 1998-03-06 Added delspilts, Addsplits, Delsplits.
1998-03-06 nipkow 1998-03-06 expand_if is now by default part of the simpset.
1998-03-05 paulson 1998-03-05 New theorem and simprules
1998-03-04 nipkow 1998-03-04 Reorganized simplifier. May now reorient rules. Moved loop tests from logic to thm.
1998-03-04 nipkow 1998-03-04 Reorganized simplifier. May now reorient rules. This breaks many of the proofs in this file. Deactivated the feature locally.
1998-03-04 nipkow 1998-03-04 Reorganized simplifier. May now reorient rules.
1998-03-03 paulson 1998-03-03 Better simplification allows deletion of parts of proofs
1998-03-03 paulson 1998-03-03 New theorem
1998-03-03 paulson 1998-03-03 New theorems
1998-03-03 paulson 1998-03-03 New theorems; tidied
1998-03-03 paulson 1998-03-03 New theorem diff_Suc_le_Suc_diff; tidied another proof
1998-03-03 paulson 1998-03-03 auto generated
1998-02-28 nipkow 1998-02-28 Modified def.
1998-02-28 nipkow 1998-02-28 Splitters via named loopers.
1998-02-28 nipkow 1998-02-28 Little reorganization. Loop tactics have names now.
1998-02-28 nipkow 1998-02-28 Tried to reorganize rewriter a little. More to be done.
1998-02-27 oheimb 1998-02-27 added minimal description of rep_cs: corrections
1998-02-27 oheimb 1998-02-27 added minimal description of rep_cs
1998-02-27 oheimb 1998-02-27 added minimal description of rep_ss
1998-02-27 paulson 1998-02-27 "choice" moved to Set.ML
1998-02-27 paulson 1998-02-27 New absorbsion laws, etc
1998-02-27 paulson 1998-02-27 Vimage
1998-02-27 paulson 1998-02-27 New vimage laws
1998-02-26 oheimb 1998-02-26 added smart_tac
1998-02-26 oheimb 1998-02-26 removed superfluous addss
1998-02-26 paulson 1998-02-26 New theory, Vimage
1998-02-26 paulson 1998-02-26 Proved choice and bchoice; changed Fun.thy -> thy
1998-02-26 wenzelm 1998-02-26 *** empty log message ***
1998-02-26 wenzelm 1998-02-26 added clasimp.ML;
1998-02-25 oheimb 1998-02-25 renamed rep_claset to rep_cs
1998-02-25 oheimb 1998-02-25 factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML explicitly introducing combined type clasimpset
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1998-02-25 oheimb 1998-02-25 added split_all_tac to claset()
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1998-02-24 paulson 1998-02-24 New theory of the inverse image of a function
1998-02-24 nipkow 1998-02-24 Added some lemmas.
1998-02-23 paulson 1998-02-23 Catches bad elim rules, handling exception OPTION
1998-02-23 paulson 1998-02-23 New laws for union
1998-02-23 paulson 1998-02-23 New laws for id
1998-02-22 nipkow 1998-02-22 New induction schemas for lists (length and snoc).
1998-02-20 nipkow 1998-02-20 *** empty log message ***
1998-02-20 nipkow 1998-02-20 Congruence rules use == in premises now.
1998-02-20 nipkow 1998-02-20 Congruence rules use == in premises now. New class linord.
1998-02-20 oheimb 1998-02-20 minor improvements
1998-02-20 oheimb 1998-02-20 re-arranged bindings for many function keys
1998-02-20 oheimb 1998-02-20 extended input syntax to handle names of special keys
1998-02-20 oheimb 1998-02-20 moved Ctrl entry before Alt entry extended input syntax to handle names of special keys
1998-02-20 paulson 1998-02-20 New theorem eq_imp_le
1998-02-19 paulson 1998-02-19 Four new Union/Intersection laws