Mon, 28 Aug 2000 20:31:00 +0200 wenzelm Method.SIMPLE_METHOD';
Mon, 28 Aug 2000 20:30:47 +0200 wenzelm 'induct_tac' / 'case_tac': Method.goal_args';
Mon, 28 Aug 2000 20:29:56 +0200 wenzelm added 'split' method;
Mon, 28 Aug 2000 20:29:19 +0200 wenzelm \newenvironment{isabellebody}: version without trivlist;
Mon, 28 Aug 2000 20:28:44 +0200 wenzelm * \isabellestyle{it} produces near math mode output;
Mon, 28 Aug 2000 17:02:19 +0200 nipkow Removed map_compose from simpset.
Mon, 28 Aug 2000 16:53:35 +0200 kleing fixed Id string
Mon, 28 Aug 2000 15:13:55 +0200 wenzelm updated;
Mon, 28 Aug 2000 14:09:33 +0200 wenzelm restart_loader: reset_path;
Mon, 28 Aug 2000 14:09:12 +0200 wenzelm add_path: del_path first;
Mon, 28 Aug 2000 13:52:38 +0200 wenzelm proper setup of iman.sty/extra.sty/ttbox.sty;
Mon, 28 Aug 2000 13:50:24 +0200 wenzelm updated;
Mon, 28 Aug 2000 13:48:47 +0200 wenzelm moved \tt things to ttbox.sty;
Mon, 28 Aug 2000 13:48:25 +0200 wenzelm proper setup;
Mon, 28 Aug 2000 13:48:14 +0200 wenzelm removed ttbox;
Mon, 28 Aug 2000 10:16:58 +0200 nipkow *** empty log message ***
Mon, 28 Aug 2000 09:32:51 +0200 nipkow *** empty log message ***
Fri, 25 Aug 2000 12:17:09 +0200 paulson added \trivlist...\endtrivlist to the "isabelle" environment
Fri, 25 Aug 2000 12:15:35 +0200 paulson moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
Thu, 24 Aug 2000 12:39:42 +0200 paulson xsymbols for {| and |}
Thu, 24 Aug 2000 12:39:24 +0200 paulson xsymbols for leads-to and Join
Thu, 24 Aug 2000 11:14:21 +0200 paulson fixed strip_assums and assum_pairs, restoring them (essentially) to their
Thu, 24 Aug 2000 11:05:20 +0200 paulson added some xsymbols, and tidied
Thu, 24 Aug 2000 00:55:42 +0200 wenzelm more symbols;
Thu, 24 Aug 2000 00:54:54 +0200 wenzelm disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);
Thu, 24 Aug 2000 00:53:53 +0200 wenzelm choosefrom: support easy settings;
Thu, 24 Aug 2000 00:53:23 +0200 wenzelm choosefrom: easy settings;
Wed, 23 Aug 2000 15:24:46 +0200 wenzelm isabelle env: trivlist;
Tue, 22 Aug 2000 11:24:44 +0200 paulson removed redundant commands
Tue, 22 Aug 2000 11:24:24 +0200 paulson removed most "makeatother", no longer needed
Tue, 22 Aug 2000 10:59:15 +0200 paulson updated to latest versions of ttbox and ttbreak
Mon, 21 Aug 2000 19:29:27 +0200 wenzelm updated;
Mon, 21 Aug 2000 19:17:07 +0200 wenzelm updated;
Mon, 21 Aug 2000 19:03:58 +0200 wenzelm updated;
Mon, 21 Aug 2000 18:49:38 +0200 wenzelm tuned translations;
Mon, 21 Aug 2000 18:45:29 +0200 nipkow *** empty log message ***
Mon, 21 Aug 2000 18:40:30 +0200 wenzelm added \isastyleminor;
Mon, 21 Aug 2000 18:38:27 +0200 wenzelm more \isachars;
Mon, 21 Aug 2000 18:16:47 +0200 wenzelm fixed has_meta_prems: strip_assums_hyp;
Mon, 21 Aug 2000 17:54:43 +0200 nipkow *** empty log message ***
Mon, 21 Aug 2000 13:47:24 +0200 wenzelm updated;
Sun, 20 Aug 2000 17:45:20 +0200 wenzelm open cases;
Sat, 19 Aug 2000 12:49:19 +0200 wenzelm output \isachar;
Sat, 19 Aug 2000 12:48:26 +0200 wenzelm cond_add_path;
Sat, 19 Aug 2000 12:47:16 +0200 wenzelm fixed text;
Sat, 19 Aug 2000 12:45:11 +0200 wenzelm turned into new-style theory;
Sat, 19 Aug 2000 12:44:39 +0200 wenzelm tuned;
Sat, 19 Aug 2000 12:44:20 +0200 wenzelm tuned \isastyle;
Sat, 19 Aug 2000 12:43:55 +0200 wenzelm added \isachar definitions;
Sat, 19 Aug 2000 12:42:52 +0200 wenzelm %\urlstyle{rm}
Sat, 19 Aug 2000 12:41:41 +0200 wenzelm renamed cond_with_path to cond_add_path (add to front);
Fri, 18 Aug 2000 18:46:02 +0200 paulson X-symbols for ordinal, cardinal, integer arithmetic
Fri, 18 Aug 2000 18:11:10 +0200 wenzelm fixed RuleCases.make (invert flag);
Fri, 18 Aug 2000 18:06:10 +0200 wenzelm removed obsolete add_recdef_x;
Fri, 18 Aug 2000 17:58:33 +0200 wenzelm proper handling of defs;
Fri, 18 Aug 2000 17:53:49 +0200 wenzelm Main now new-style theory; added Main.ML for compatibility;
Fri, 18 Aug 2000 12:34:48 +0200 paulson simproc bug fix: only TYPING assumptions are given to the simplifier
Fri, 18 Aug 2000 12:34:13 +0200 paulson better rules for cancellation of common factors across comparisons
Fri, 18 Aug 2000 12:31:20 +0200 paulson new example ZF/ex/NatSum
Fri, 18 Aug 2000 12:30:41 +0200 paulson now allows dest_coeff to fail
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip