2000-08-29 wenzelm added prems_limit;
2000-08-29 wenzelm added "name" antiq and "indent" option;
2000-08-29 wenzelm pr: added prems limit;
2000-08-29 wenzelm added indent;
2000-08-29 wenzelm \<dots> syntax;
2000-08-29 wenzelm added antiquotation 'name' and option 'indent';
2000-08-29 wenzelm 'syntax': improved mode spec;
2000-08-29 wenzelm improved spacing of Sum, Prod, integral;
2000-08-29 wenzelm underscore: added \mbox to avoid hyphenation;
2000-08-29 wenzelm * 'pr' command: optional argument for ProofContext.prems_limit;
2000-08-29 nipkow *** empty log message ***
2000-08-29 nipkow *** empty log message ***
2000-08-29 nipkow *** empty log message ***
2000-08-29 wenzelm made SML/XL happy;
2000-08-29 wenzelm updated;
2000-08-29 wenzelm improved isabellepar env;
2000-08-29 wenzelm updated;
2000-08-28 wenzelm Lambda/InductTermi made new-style theory;
2000-08-28 wenzelm proper cong setup;
2000-08-28 wenzelm Simplifier.cong_add_global;
2000-08-28 wenzelm cong setup now part of Simplifier;
2000-08-28 wenzelm updated cong stuff;
2000-08-28 wenzelm 'cong' modifiers;
2000-08-28 wenzelm \isakeywordcharunderscore;
2000-08-28 wenzelm * Isar/Provers: 'simp' method now supports 'cong' modifiers;
2000-08-28 wenzelm tex_index: Latex.tex_trailer;
2000-08-28 wenzelm added tex_trailer;
2000-08-28 wenzelm removed METHOD0;
2000-08-28 wenzelm Method.SIMPLE_METHOD';
2000-08-28 wenzelm 'induct_tac' / 'case_tac': Method.goal_args';
2000-08-28 wenzelm added 'split' method;
2000-08-28 wenzelm \newenvironment{isabellebody}: version without trivlist;
2000-08-28 wenzelm * \isabellestyle{it} produces near math mode output;
2000-08-28 nipkow Removed map_compose from simpset.
2000-08-28 kleing fixed Id string
2000-08-28 wenzelm updated;
2000-08-28 wenzelm restart_loader: reset_path;
2000-08-28 wenzelm add_path: del_path first;
2000-08-28 wenzelm proper setup of iman.sty/extra.sty/ttbox.sty;
2000-08-28 wenzelm updated;
2000-08-28 wenzelm moved \tt things to ttbox.sty;
2000-08-28 wenzelm proper setup;
2000-08-28 wenzelm removed ttbox;
2000-08-28 nipkow *** empty log message ***
2000-08-28 nipkow *** empty log message ***
2000-08-25 paulson added \trivlist...\endtrivlist to the "isabelle" environment
2000-08-25 paulson moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
2000-08-24 paulson xsymbols for {| and |}
2000-08-24 paulson xsymbols for leads-to and Join
2000-08-24 paulson fixed strip_assums and assum_pairs, restoring them (essentially) to their
2000-08-24 paulson added some xsymbols, and tidied
2000-08-23 wenzelm more symbols;
2000-08-23 wenzelm disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);
2000-08-23 wenzelm choosefrom: support easy settings;
2000-08-23 wenzelm choosefrom: easy settings;
2000-08-23 wenzelm isabelle env: trivlist;
2000-08-22 paulson removed redundant commands
2000-08-22 paulson removed most "makeatother", no longer needed
2000-08-22 paulson updated to latest versions of ttbox and ttbreak
2000-08-21 wenzelm updated;
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip