2002-02-14 nipkow 2002-02-14 nodups -> distinct
2002-02-14 nipkow 2002-02-14 nodups -> distinct
2002-02-13 paulson 2002-02-13 deleted some redundant 'addS*Es [equalityC*E]'s
2002-02-13 paulson 2002-02-13 new function lemmas
2002-02-13 paulson 2002-02-13 tidied. no more special simpset (super_ss)
2002-02-13 paulson 2002-02-13 new lemmas for closure under Union
2002-02-12 wenzelm 2002-02-12 eliminated Pure/Isar/comment.ML;
2002-02-12 wenzelm 2002-02-12 ANTIQUOTE_FAIL;
2002-02-12 wenzelm 2002-02-12 eliminated Isar/comment.ML;
2002-02-12 wenzelm 2002-02-12 tuned;
2002-02-12 wenzelm 2002-02-12 added isabelle-hol-book; added tphols2001; tuned tphols2000;
2002-02-12 wenzelm 2002-02-12 * Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text;
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2002-02-12 wenzelm 2002-02-12 tuned;
2002-02-11 wenzelm 2002-02-11 ML-Systems/smlnj-compiler.ML compatibility tweak;
2002-02-11 wenzelm 2002-02-11 include SVC_Test;
2002-02-07 berghofe 2002-02-07 Theorems are only "pre-named" if the do not already have names.
2002-02-06 berghofe 2002-02-06 Added function could_unify to speed up rewriting of proof terms.
2002-02-06 berghofe 2002-02-06 Indexes of variables in expanded proofs are now incremented to avoid clashes.
2002-02-05 wenzelm 2002-02-05 moved SVC stuff to ex;
2002-02-05 berghofe 2002-02-05 New function maxidx_of_proof.
2002-02-04 paulson 2002-02-04 New-style versions of these old examples
2002-02-02 berghofe 2002-02-02 Rewrite procedure now works for both compact and full proof objects.
2002-01-30 wenzelm 2002-01-30 escape_mfix;
2002-01-30 wenzelm 2002-01-30 added literal;
2002-01-30 wenzelm 2002-01-30 prep_mixfix': proper use of Syntax.literal;
2002-01-30 wenzelm 2002-01-30 tuned;
2002-01-30 paulson 2002-01-30 mu-syntax for the LEAST operator
2002-01-30 paulson 2002-01-30 Multiset: added the translation Mult(A) => A-||>nat-{0} (which internalises the `multiset' relation). FoldSet: weakened the typing conditions of the function f and (by the way) removed the `locale' declarations.
2002-01-28 wenzelm 2002-01-28 tuned;
2002-01-28 wenzelm 2002-01-28 GPLed;
2002-01-28 wenzelm 2002-01-28 tuned header;
2002-01-28 wenzelm 2002-01-28 tuned;
2002-01-28 schirmer 2002-01-28 Bali added
2002-01-28 schirmer 2002-01-28 Isabelle/Bali sources;
2002-01-26 wenzelm 2002-01-26 Isar cases/induct: no backtracking;
2002-01-26 wenzelm 2002-01-26 cases: really append cases_default; cases/induct method: DETERM;
2002-01-26 wenzelm 2002-01-26 generic DETERM;
2002-01-25 paulson 2002-01-25 ZF
2002-01-24 wenzelm 2002-01-24 copy_files *.sty;
2002-01-24 wenzelm 2002-01-24 cond_print_result_rule: priority (again) instead of slightly ill-behaved tracing output;
2002-01-24 wenzelm 2002-01-24 fixed subgoal_tac; fails on non-existent subgoal;
2002-01-24 wenzelm 2002-01-24 copy_styles replaces overly conservative update_styles;
2002-01-24 wenzelm 2002-01-24 Springer LNCS 2283;
2002-01-24 wenzelm 2002-01-24 updated;
2002-01-24 wenzelm 2002-01-24 iff del: less_Suc0 -- luckily this does NOT affect the printed text;
2002-01-23 wenzelm 2002-01-23 delsimps [less_Suc0];
2002-01-23 wenzelm 2002-01-23 less_Suc0;
2002-01-23 wenzelm 2002-01-23 error "Unexpected end of input";
2002-01-23 wenzelm 2002-01-23 reorganized code for predicate text;
2002-01-23 wenzelm 2002-01-23 tuned; lemmas nat_number_of;
2002-01-23 wenzelm 2002-01-23 * HOL: nat_number_of;
2002-01-23 paulson 2002-01-23 A few more standard simprules, TCs, etc.
2002-01-22 wenzelm 2002-01-22 qualified_result replaces qualified;
2002-01-22 wenzelm 2002-01-22 added locale_facts(_i) interface (useful for simple ML proof tools);
2002-01-21 wenzelm 2002-01-21 full_proofs;
2002-01-21 wenzelm 2002-01-21 * Pure/show_hyps reset by default (in accordance to existing Isar practice);
2002-01-21 wenzelm 2002-01-21 reset show_hyps by default (in accordance to existing Isar practice);
2002-01-21 wenzelm 2002-01-21 save library;
2002-01-21 wenzelm 2002-01-21 full_atomize;