Mon, 07 Feb 2000 18:40:40 +0100 wenzelm assert_no_chain;
Mon, 07 Feb 2000 18:40:27 +0100 wenzelm refine_no_facts: recover goal_facts;
Mon, 07 Feb 2000 18:39:53 +0100 wenzelm tuned prefer/defer;
Mon, 07 Feb 2000 18:38:51 +0100 wenzelm intro/elim/dest attributes: changed ! / !! flags to ? / ??;
Mon, 07 Feb 2000 15:28:43 +0100 oheimb paper available
Mon, 07 Feb 2000 15:14:02 +0100 paulson tidied some proofs
Sat, 05 Feb 2000 17:31:53 +0100 kleing Branch: top elements of stack only need to be convertible (not equal)
Sat, 05 Feb 2000 17:06:27 +0100 wenzelm tuned;
Sat, 05 Feb 2000 16:59:50 +0100 wenzelm -I option;
Sat, 05 Feb 2000 16:58:58 +0100 wenzelm -D PATH: dump generated document sources into PATH;
Sat, 05 Feb 2000 16:57:02 +0100 wenzelm additional tex dump;
Sat, 05 Feb 2000 16:54:27 +0100 wenzelm '.' == by this;
Fri, 04 Feb 2000 21:53:36 +0100 wenzelm misc improvements;
Fri, 04 Feb 2000 21:45:57 +0100 wenzelm added MicroJava/document;
Fri, 04 Feb 2000 21:44:38 +0100 wenzelm added old_symbol_source;
Fri, 04 Feb 2000 21:44:04 +0100 wenzelm Present.old_symbol_source;
Fri, 04 Feb 2000 21:43:30 +0100 wenzelm tuned;
Fri, 04 Feb 2000 21:37:23 +0100 wenzelm manually load session;
Fri, 04 Feb 2000 21:36:13 +0100 wenzelm tuned syms;
Fri, 04 Feb 2000 11:36:11 +0100 paulson new theorem gcd_add_mult
Wed, 02 Feb 2000 20:19:25 +0100 wenzelm most_general_varify_tfrees all results;
Wed, 02 Feb 2000 13:26:38 +0100 nipkow Rduced Class C <= Class D to C <= D.
Wed, 02 Feb 2000 12:46:57 +0100 wenzelm nat as names;
Wed, 02 Feb 2000 12:25:54 +0100 paulson expandshort
Wed, 02 Feb 2000 12:25:29 +0100 paulson new lemma fun_cons_restrict_eq
Wed, 02 Feb 2000 11:42:17 +0100 paulson new theorems by Sidi O. Ehmety
Tue, 01 Feb 2000 18:18:36 +0100 oheimb added forgotten definition of make_imp_tac
Tue, 01 Feb 2000 18:18:09 +0100 oheimb added forgotten rules to make IMPP
Tue, 01 Feb 2000 12:26:47 +0100 wenzelm eliminated nonascii;
Mon, 31 Jan 2000 18:30:35 +0100 oheimb added IMPP to HOL
Mon, 31 Jan 2000 16:19:51 +0100 paulson renamed image_Union_eq -> image_Union
Mon, 31 Jan 2000 16:19:14 +0100 paulson new theorem vimage_Union
Mon, 31 Jan 2000 16:18:42 +0100 paulson new theorem rev_ImageI
Mon, 31 Jan 2000 16:18:09 +0100 paulson various theorems about image and inverse image
Mon, 31 Jan 2000 16:13:28 +0100 paulson Pi_empty1 is a more general simprule than empty_fun
Sun, 30 Jan 2000 13:24:41 +0100 wenzelm rm -f *.aux;
Sat, 29 Jan 2000 14:22:16 +0100 wenzelm simp_all method;
Fri, 28 Jan 2000 21:58:39 +0100 wenzelm eliminated proof script;
Fri, 28 Jan 2000 21:57:15 +0100 wenzelm HEADGOAL;
Fri, 28 Jan 2000 21:56:55 +0100 wenzelm added prefer, defer;
Fri, 28 Jan 2000 21:56:37 +0100 wenzelm added HEADGOAL;
Fri, 28 Jan 2000 21:56:02 +0100 wenzelm added defer, prefer;
Fri, 28 Jan 2000 21:55:43 +0100 wenzelm Drule.instantiate;
Fri, 28 Jan 2000 21:55:23 +0100 wenzelm cp -r;
Fri, 28 Jan 2000 15:26:51 +0100 wenzelm -p option;
Fri, 28 Jan 2000 15:08:15 +0100 oheimb added range_composition (also to simpset)
Fri, 28 Jan 2000 14:49:00 +0100 oheimb added finite_range_updI, finite_range_map_of, finite_range_map_of_override
Fri, 28 Jan 2000 14:42:46 +0100 wenzelm mkdir: prepare logic session directory;
Fri, 28 Jan 2000 14:09:23 +0100 oheimb added full_nat_induct
Fri, 28 Jan 2000 14:08:54 +0100 oheimb added splitE', also to claset
Fri, 28 Jan 2000 14:07:53 +0100 oheimb added inj_singleton
Fri, 28 Jan 2000 14:07:33 +0100 oheimb added finite_range_imageI
Fri, 28 Jan 2000 12:12:06 +0100 wenzelm replaced FIRSTGOAL by FINDGOAL (backtracking!);
Fri, 28 Jan 2000 12:10:47 +0100 wenzelm maintain standard rules (beware: classical provers provides another version!);
Fri, 28 Jan 2000 12:06:52 +0100 wenzelm replaced FIRSTGOAL by FINDGOAL (backtracking!);
Fri, 28 Jan 2000 12:04:17 +0100 wenzelm tuned sig;
Fri, 28 Jan 2000 12:03:59 +0100 wenzelm map data;
Fri, 28 Jan 2000 11:23:41 +0100 oheimb added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
Fri, 28 Jan 2000 11:22:02 +0100 oheimb beautified spacing for binders with symbols syntax, analogous to HOL.thy
Thu, 27 Jan 2000 15:30:10 +0100 oheimb *** empty log message ***
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip