1997-10-20 wenzelm 1997-10-20 tuned output;
1997-10-20 wenzelm 1997-10-20 adapted to qualified names;
1997-10-20 wenzelm 1997-10-20 Sign.base_name;
1997-10-20 wenzelm 1997-10-20 fixed types of add_XXX;
1997-10-20 wenzelm 1997-10-20 local;
1997-10-20 wenzelm 1997-10-20 local section; improved global, local;
1997-10-18 nipkow 1997-10-18 addsplits
1997-10-17 wenzelm 1997-10-17 adapted to qualified names;
1997-10-17 wenzelm 1997-10-17 no longer tries bogus eta-contract involving aprops;
1997-10-17 wenzelm 1997-10-17 adapted to qualified names;
1997-10-17 wenzelm 1997-10-17 fixed RAW target;
1997-10-17 wenzelm 1997-10-17 (co) inductive / datatype package adapted to qualified names;
1997-10-17 wenzelm 1997-10-17 obselete 'end' hack;
1997-10-17 wenzelm 1997-10-17 global;
1997-10-17 wenzelm 1997-10-17 tuned "." syntax;
1997-10-17 wenzelm 1997-10-17 removed Classlib;
1997-10-17 wenzelm 1997-10-17 *** empty log message ***
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-17 nipkow 1997-10-17 Added error messages.
1997-10-17 paulson 1997-10-17 A lot of new comments
1997-10-17 paulson 1997-10-17 Eta-expanded a function decl to make sml/nj happy
1997-10-17 paulson 1997-10-17 Added "op" before "occs" to make sml/nj happy
1997-10-17 paulson 1997-10-17 New rewrite rules for simplifying conditionals
1997-10-17 paulson 1997-10-17 New trivial rewrites
1997-10-17 paulson 1997-10-17 New rewrite rules for simplifying conditionals
1997-10-17 paulson 1997-10-17 Better simplification eliminates a command from proof of psubset_card
1997-10-17 paulson 1997-10-17 New simprules imp_disj1,2 and some comments
1997-10-17 nipkow 1997-10-17 Added image_eqI to simpset.
1997-10-17 nipkow 1997-10-17 Removed image_eqI from simpset because of clash with neq_shrK.
1997-10-16 nipkow 1997-10-16 AddIffs [all_not_in_conv];
1997-10-16 wenzelm 1997-10-16 global;
1997-10-16 nipkow 1997-10-16 Modified comment.
1997-10-16 paulson 1997-10-16 New simprules imp_disj1, imp_disj2
1997-10-16 paulson 1997-10-16 New simprule diff_le_self, requiring a new proof of diff_diff_cancel
1997-10-16 nipkow 1997-10-16 Removed comment.
1997-10-16 wenzelm 1997-10-16 tuned;
1997-10-16 wenzelm 1997-10-16 removed begin; added global section; added global_names flag (tmp), default true;
1997-10-16 wenzelm 1997-10-16 fixed prep_ext;
1997-10-16 nipkow 1997-10-16 Simplified proof.
1997-10-16 nipkow 1997-10-16 Simplified proof because of better simplifier.
1997-10-16 nipkow 1997-10-16 Various new lemmas. Improved conversion of equations to rewrite rules: (s=t becomes (s=t)==True if s=t loops).
1997-10-16 wenzelm 1997-10-16 added transfer: theory -> thm -> thm;
1997-10-16 wenzelm 1997-10-16 oops;
1997-10-16 nipkow 1997-10-16 The simplifier has been improved a little: equations s=t which used to be rejected because of looping are now treated as (s=t) == True. The latter translation must be done outside of Thm because it involves the object-logic specific True. Therefore the simple loop test has been moved from Thm to Logic.
1997-10-16 wenzelm 1997-10-16 fixed dependencies;
1997-10-16 wenzelm 1997-10-16 transfer thy Ord_nat;
1997-10-16 wenzelm 1997-10-16 sevaral goals restated in mono.thy;
1997-10-16 wenzelm 1997-10-16 moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;
1997-10-16 wenzelm 1997-10-16 transfer InfDatatype.thy Limit_VfromE;
1997-10-16 wenzelm 1997-10-16 transfer CardinalArith.thy nat_into_Ord;
1997-10-16 wenzelm 1997-10-16 improved pretty_arity;
1997-10-16 wenzelm 1997-10-16 added merge_theories (new name arg);
1997-10-16 wenzelm 1997-10-16 fixed merge_theories;
1997-10-16 wenzelm 1997-10-16 revert to 1.3;
1997-10-16 wenzelm 1997-10-16 revert to 1.1;
1997-10-16 nipkow 1997-10-16 Added last, butlast, dropped ttl.
1997-10-16 mueller 1997-10-16 lala
1997-10-16 paulson 1997-10-16 Eta-expansion of function declarations, for value polymorphism
1997-10-15 wenzelm 1997-10-15 remove merge_theories; merge_list: always prepares extend -- no longer supports aliasing merges;
1997-10-15 wenzelm 1997-10-15 make_draft replaced by prep_ext; improved print_data; merge now does trivial (absorptive) merges only; added nontriv_merge;