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;
2002-01-21 wenzelm 2002-01-21 wild guess at polyml-4.1.2;
2002-01-21 wenzelm 2002-01-21 options -l and -t; tuned;
2002-01-21 berghofe 2002-01-21 Removed timing function.
2002-01-21 paulson 2002-01-21 new simprules and classical rules
2002-01-21 berghofe 2002-01-21 Tuned name mangling function.
2002-01-21 berghofe 2002-01-21 Made some proofs constructive.
2002-01-21 berghofe 2002-01-21 datatype_codegen now checks type of constructor.
2002-01-21 nipkow 2002-01-21 *** empty log message ***
2002-01-21 paulson 2002-01-21 lexical tidying
2002-01-21 paulson 2002-01-21 slight re-use of code
2002-01-19 kleing 2002-01-19 fixed typos
2002-01-18 wenzelm 2002-01-18 rewrite_term: removed rew0, so no on-the-fly eta-contraction;
2002-01-18 wenzelm 2002-01-18 fixed document setup of HOL-Library;
2002-01-18 wenzelm 2002-01-18 tuned;
2002-01-18 paulson 2002-01-18 tidied
2002-01-18 paulson 2002-01-18 OOPS
2002-01-18 paulson 2002-01-18 tweaks
2002-01-18 wenzelm 2002-01-18 moved document sources to proper place, *within* Library/Library (!);
2002-01-17 wenzelm 2002-01-17 cover polyml-4.1.2;
2002-01-17 wenzelm 2002-01-17 RuleCases.make interface based on term instead of thm;
2002-01-17 wenzelm 2002-01-17 RuleCases.make interface based on term instead of thm; tuned;
2002-01-17 wenzelm 2002-01-17 atomize_term replaces atomize_cterm;
2002-01-17 wenzelm 2002-01-17 ObjectLogic.atomize_term replaces ObjectLogic.atomize_cterm;
2002-01-17 wenzelm 2002-01-17 Thm.prop_of;
2002-01-17 wenzelm 2002-01-17 Tactic.norm_hhf renamed to Tactic.norm_hhf_rule;
2002-01-17 wenzelm 2002-01-17 added prop_of: thm -> term (at last!);
2002-01-17 wenzelm 2002-01-17 added add_term_free_names (more precise/efficient than add_term_names);
2002-01-17 wenzelm 2002-01-17 renamed norm_hhf to norm_hhf_rule; removed slow rewrite_cterm;
2002-01-17 wenzelm 2002-01-17 added is_norm_hhf (from logic.ML); norm_hhf based on fast Pattern.rewrite_term;
2002-01-17 wenzelm 2002-01-17 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm; RuleCases.make interface based on term instead of thm;
2002-01-17 wenzelm 2002-01-17 MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;