2000-08-22 paulson 2000-08-22 updated to latest versions of ttbox and ttbreak
2000-08-21 wenzelm 2000-08-21 updated;
2000-08-21 wenzelm 2000-08-21 updated;
2000-08-21 wenzelm 2000-08-21 updated;
2000-08-21 wenzelm 2000-08-21 tuned translations;
2000-08-21 nipkow 2000-08-21 *** empty log message ***
2000-08-21 wenzelm 2000-08-21 added \isastyleminor; more \isachars; added \isadigit; improved \isakeyword; tuned;
2000-08-21 wenzelm 2000-08-21 more \isachars; added \isadigit; simplified command markup;
2000-08-21 wenzelm 2000-08-21 fixed has_meta_prems: strip_assums_hyp;
2000-08-21 nipkow 2000-08-21 *** empty log message ***
2000-08-21 wenzelm 2000-08-21 updated;
2000-08-20 wenzelm 2000-08-20 open cases;
2000-08-19 wenzelm 2000-08-19 output \isachar;
2000-08-19 wenzelm 2000-08-19 cond_add_path;
2000-08-19 wenzelm 2000-08-19 fixed text;
2000-08-19 wenzelm 2000-08-19 turned into new-style theory;
2000-08-19 wenzelm 2000-08-19 tuned;
2000-08-19 wenzelm 2000-08-19 tuned \isastyle;
2000-08-19 wenzelm 2000-08-19 added \isachar definitions; added \isabellestyle switch; tuned;
2000-08-19 wenzelm 2000-08-19 %\urlstyle{rm} %\isabellestyle{it}
2000-08-19 wenzelm 2000-08-19 renamed cond_with_path to cond_add_path (add to front); improved with_path(s) (add to rear);
2000-08-18 paulson 2000-08-18 X-symbols for ordinal, cardinal, integer arithmetic
2000-08-18 wenzelm 2000-08-18 fixed RuleCases.make (invert flag);
2000-08-18 wenzelm 2000-08-18 removed obsolete add_recdef_x;
2000-08-18 wenzelm 2000-08-18 proper handling of defs;
2000-08-18 wenzelm 2000-08-18 Main now new-style theory; added Main.ML for compatibility;
2000-08-18 paulson 2000-08-18 simproc bug fix: only TYPING assumptions are given to the simplifier
2000-08-18 paulson 2000-08-18 better rules for cancellation of common factors across comparisons
2000-08-18 paulson 2000-08-18 new example ZF/ex/NatSum
2000-08-18 paulson 2000-08-18 now allows dest_coeff to fail
2000-08-18 nipkow 2000-08-18 *** empty log message ***
2000-08-18 nipkow 2000-08-18 *** empty log message ***
2000-08-17 wenzelm 2000-08-17 removed obsolete keyword;
2000-08-17 wenzelm 2000-08-17 fixed indexing;
2000-08-17 wenzelm 2000-08-17 tuned;
2000-08-17 nipkow 2000-08-17 installed recdef congs data
2000-08-17 nipkow 2000-08-17 added map_cong to recdef
2000-08-17 wenzelm 2000-08-17 removed Lambda/Type.ML;
2000-08-17 paulson 2000-08-17 better rules for cancellation of common factors across comparisons
2000-08-17 paulson 2000-08-17 fixed a proof that had stopped working ???
2000-08-17 paulson 2000-08-17 tidied & updated proofs, deleting some unused ones
2000-08-17 paulson 2000-08-17 modified proofs: better rules for cancellation of common factors across comparisons
2000-08-17 paulson 2000-08-17 better rules for cancellation of common factors across comparisons
2000-08-17 wenzelm 2000-08-17 *** empty log message ***
2000-08-17 wenzelm 2000-08-17 cases: opaque by default; fixed ML tactic: proper context; added 'rename_tac', 'rename_tac';
2000-08-17 wenzelm 2000-08-17 renamed 'RS' to 'THEN';
2000-08-17 wenzelm 2000-08-17 tuned error handling;
2000-08-17 wenzelm 2000-08-17 added 'symmetric' attribute;
2000-08-17 wenzelm 2000-08-17 updated; tuned;
2000-08-17 wenzelm 2000-08-17 sel_upd proc: include 'more' pseudo-field; added equality rule;
2000-08-17 wenzelm 2000-08-17 renamed 'mk_cases_tac' to 'ind_cases';
2000-08-17 wenzelm 2000-08-17 changed 'opaque' option to 'open' (opaque is default); renamed 'mk_cases_tac' to 'ind_cases';
2000-08-17 wenzelm 2000-08-17 renamed 'RS' to 'THEN'; 'symmetric' attribute;
2000-08-17 wenzelm 2000-08-17 converted to new-style theory;
2000-08-17 wenzelm 2000-08-17 done;
2000-08-17 wenzelm 2000-08-17 'symmetric' attribute;
2000-08-17 wenzelm 2000-08-17 fixed deps;
2000-08-17 wenzelm 2000-08-17 renamed 'RS' to 'THEN';
2000-08-17 wenzelm 2000-08-17 index tokens; added 'int';
2000-08-17 wenzelm 2000-08-17 cases/induct method: 'opaque' by default; added 'open' option;