1998-11-21 wenzelm 1998-11-21 std_output, prefix_lines;
1998-11-20 paulson 1998-11-20 better miniscoping rules: the premise C~={} is not good because Safe_tac eliminates such assumptions.
1998-11-19 wenzelm 1998-11-19 fixed method syntax;
1998-11-19 wenzelm 1998-11-19 break: exhibit state stack;
1998-11-19 wenzelm 1998-11-19 match_bind: 'as' patterns; statements: 'is' patterns;
1998-11-19 wenzelm 1998-11-19 let: 'as' patterns; statements: propp ('is' patterns);
1998-11-19 wenzelm 1998-11-19 match_bind(_i): 'as' patterns; assume, theorem, show etc.: propp; tuned qed msg;
1998-11-19 wenzelm 1998-11-19 term_pat vs. prop_pat; added bind_propp(_i); assume: propp;
1998-11-19 wenzelm 1998-11-19 term_pat vs. prop_pat;
1998-11-19 wenzelm 1998-11-19 no warning for "it" theorems;
1998-11-18 paulson 1998-11-18 tidied
1998-11-18 paulson 1998-11-18 Finally removing "Compl" from HOL
1998-11-18 wenzelm 1998-11-18 exn_message FAIL;
1998-11-18 wenzelm 1998-11-18 blast: cla_method';
1998-11-18 wenzelm 1998-11-18 export simp_modifiers;
1998-11-18 wenzelm 1998-11-18 expoer cla_method('), cla_modifiers;
1998-11-18 wenzelm 1998-11-18 method setup;
1998-11-18 wenzelm 1998-11-18 tuned comments;
1998-11-18 wenzelm 1998-11-18 'prop', 'term', 'typ';
1998-11-18 wenzelm 1998-11-18 load;
1998-11-18 wenzelm 1998-11-18 export exn_message;
1998-11-18 wenzelm 1998-11-18 removed trace;
1998-11-17 wenzelm 1998-11-17 BREAK: include state; report Attrib.ATTRIB_FAIL, Method.METHOD_FAIL;
1998-11-17 wenzelm 1998-11-17 have_tthms; assume: store actual asms;
1998-11-17 wenzelm 1998-11-17 PureThy.default_name; have_tthms;
1998-11-17 wenzelm 1998-11-17 generalized (opt_)thm_name; xthm, xthms1;
1998-11-17 wenzelm 1998-11-17 exception METHOD_FAIL;
1998-11-17 wenzelm 1998-11-17 added have_theorems, have_lemmas, have_facts; tuned from_facts; Theory.apply replaced by Library.apply;
1998-11-17 wenzelm 1998-11-17 added 'theorems', 'lemmas', 'note'; tuned 'thm';
1998-11-17 wenzelm 1998-11-17 break: exhibit state; removed print_thm;
1998-11-17 wenzelm 1998-11-17 exception ATTRIB_FAIL; local_attribute'; removed 'lemma', 'assumption'; added 'where', 'with';
1998-11-17 wenzelm 1998-11-17 removed trace;
1998-11-17 wenzelm 1998-11-17 Symbol.space;
1998-11-17 wenzelm 1998-11-17 space;
1998-11-17 wenzelm 1998-11-17 val spc: int -> T;
1998-11-17 wenzelm 1998-11-17 added default_name; added have_tthmss;
1998-11-17 wenzelm 1998-11-17 Drule.rev_triv_goal;
1998-11-17 wenzelm 1998-11-17 Theory.apply replaced by Library.apply;
1998-11-17 wenzelm 1998-11-17 val apply: ('a -> 'a) list -> 'a -> 'a; val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b;
1998-11-17 wenzelm 1998-11-17 export vars_of and friends; open BasicDrule only;
1998-11-17 wenzelm 1998-11-17 Pretty.spc;
1998-11-17 wenzelm 1998-11-17 added pretty_tthms, print_tthms; tuned apply(s);
1998-11-17 paulson 1998-11-17 new theory UNITY/PPROD
1998-11-16 paulson 1998-11-16 new theory PPROD
1998-11-16 paulson 1998-11-16 a faster proof
1998-11-16 wenzelm 1998-11-16 removed genelim.ML;
1998-11-16 wenzelm 1998-11-16 thm, thms;
1998-11-16 wenzelm 1998-11-16 added print_thm;
1998-11-16 wenzelm 1998-11-16 made SML/NJ happy;
1998-11-16 wenzelm 1998-11-16 added oo, ooo (*concatenation: 2 and 3 args*);
1998-11-16 wenzelm 1998-11-16 Attribute.tthms_of; Theory.copy;
1998-11-16 wenzelm 1998-11-16 Attribute.tthms_of;
1998-11-16 wenzelm 1998-11-16 Attribute.thms_of;
1998-11-16 wenzelm 1998-11-16 Classical.setup, attrib_setup;
1998-11-16 wenzelm 1998-11-16 attrib_setup: rulify;
1998-11-16 wenzelm 1998-11-16 attrib_setup;
1998-11-16 wenzelm 1998-11-16 all modifiers turned into attributes; realistic method syntax; smart_simp method;
1998-11-16 wenzelm 1998-11-16 tuned attribute names; all modifiers turned into attributes; realistic method syntax;
1998-11-16 wenzelm 1998-11-16 several args parsers; realistic syntax; tuned;
1998-11-16 wenzelm 1998-11-16 tuned names;