2000-08-28 wenzelm 2000-08-28 proper setup of iman.sty/extra.sty/ttbox.sty;
2000-08-28 wenzelm 2000-08-28 updated;
2000-08-28 wenzelm 2000-08-28 moved \tt things to ttbox.sty; removed \Pure etc;
2000-08-28 wenzelm 2000-08-28 proper setup;
2000-08-28 wenzelm 2000-08-28 removed ttbox;
2000-08-28 nipkow 2000-08-28 *** empty log message ***
2000-08-28 nipkow 2000-08-28 *** empty log message ***
2000-08-25 paulson 2000-08-25 added \trivlist...\endtrivlist to the "isabelle" environment in order to correct several problems (e.g. need for newlines and %)
2000-08-25 paulson 2000-08-25 moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
2000-08-24 paulson 2000-08-24 xsymbols for {| and |}
2000-08-24 paulson 2000-08-24 xsymbols for leads-to and Join
2000-08-24 paulson 2000-08-24 fixed strip_assums and assum_pairs, restoring them (essentially) to their 1989 versions. They had been "optimized" for flattened parameters, but failed when given an initial, non-flattened proof state. A manifestation of the bug is Goal "of the bug isf. EX B. Q(f,B) ==> (of the bug isy. P(f,y))"; be exE 1;
2000-08-24 paulson 2000-08-24 added some xsymbols, and tidied
2000-08-24 wenzelm 2000-08-24 more symbols;
2000-08-24 wenzelm 2000-08-24 disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);
2000-08-24 wenzelm 2000-08-24 choosefrom: support easy settings;
2000-08-24 wenzelm 2000-08-24 choosefrom: easy settings;
2000-08-23 wenzelm 2000-08-23 isabelle env: trivlist;
2000-08-22 paulson 2000-08-22 removed redundant commands
2000-08-22 paulson 2000-08-22 removed most "makeatother", no longer needed
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 ???