Thu, 13 Jul 2000 23:22:26 +0200 wenzelm HOL: the disjoint sum is now "<+>" instead of "Plus";
Thu, 13 Jul 2000 23:20:57 +0200 wenzelm adapted PureThy.add_defs_i;
Thu, 13 Jul 2000 23:20:33 +0200 wenzelm defs (overloaded);
Thu, 13 Jul 2000 23:20:14 +0200 wenzelm tuned;
Thu, 13 Jul 2000 23:19:40 +0200 wenzelm added read_xnum;
Thu, 13 Jul 2000 23:19:08 +0200 wenzelm fix(_i): admit internal variables;
Thu, 13 Jul 2000 23:18:36 +0200 wenzelm use ProofContext.bind_skolem;
Thu, 13 Jul 2000 23:17:44 +0200 wenzelm defs: (overloaded) option;
Thu, 13 Jul 2000 23:17:14 +0200 wenzelm eq_prop: strip_assums_concl;
Thu, 13 Jul 2000 23:16:48 +0200 wenzelm tuned exceptions;
Thu, 13 Jul 2000 23:16:13 +0200 wenzelm const_deps: unit Graph.T;
Thu, 13 Jul 2000 23:15:20 +0200 wenzelm add_term_consts: ins_string;
Thu, 13 Jul 2000 23:14:49 +0200 wenzelm add_defs(_i): overloaded option;
Thu, 13 Jul 2000 23:14:15 +0200 wenzelm adapted PureThy.add_defs;
Thu, 13 Jul 2000 23:13:52 +0200 wenzelm fixed comment;
Thu, 13 Jul 2000 23:13:10 +0200 wenzelm adapted PureThy.add_defs_i;
Thu, 13 Jul 2000 23:11:38 +0200 wenzelm use Syntax.read_xnum;
Thu, 13 Jul 2000 23:11:14 +0200 wenzelm fixed simplified_cases;
Thu, 13 Jul 2000 23:10:12 +0200 wenzelm fixed name: UN_empty3;
Thu, 13 Jul 2000 23:09:25 +0200 wenzelm replaced infix Plus by <+>;
Thu, 13 Jul 2000 23:09:03 +0200 wenzelm removed duplicate Compl_atMost;
Thu, 13 Jul 2000 23:08:42 +0200 wenzelm fixed compose decl;
Thu, 13 Jul 2000 23:08:20 +0200 wenzelm defs: (overloaded) option;
Thu, 13 Jul 2000 23:07:56 +0200 wenzelm method cases/induct: (opaque) option;
Thu, 13 Jul 2000 23:07:10 +0200 wenzelm defs (overloaded);
Thu, 13 Jul 2000 13:05:58 +0200 paulson removed now-redundant proof steps
Thu, 13 Jul 2000 13:04:48 +0200 paulson added an important default rule
Thu, 13 Jul 2000 13:02:20 +0200 paulson fixed a failing proof
Thu, 13 Jul 2000 13:00:22 +0200 paulson le_refl_iff as default rule
Thu, 13 Jul 2000 12:59:26 +0200 paulson removed needless premises
Thu, 13 Jul 2000 12:56:42 +0200 paulson AddIffs now available for FOL, ZF
Thu, 13 Jul 2000 11:44:02 +0200 wenzelm added simp_case_tac;
Thu, 13 Jul 2000 11:42:11 +0200 wenzelm use InductMethod.simp_case_tac;
Thu, 13 Jul 2000 11:41:40 +0200 wenzelm tuned;
Thu, 13 Jul 2000 11:41:06 +0200 wenzelm export thesisN separately;
Thu, 13 Jul 2000 11:40:49 +0200 wenzelm prep rhs in original context;
Thu, 13 Jul 2000 11:39:41 +0200 wenzelm RuleCases.make opaq;
Thu, 13 Jul 2000 11:39:22 +0200 wenzelm bind_skolem;
Thu, 13 Jul 2000 11:39:03 +0200 wenzelm invoke_case: bind_skolem;
Thu, 13 Jul 2000 11:38:42 +0200 wenzelm "_i" arguments now expected to have skolems already internalized;
Thu, 13 Jul 2000 11:36:57 +0200 wenzelm make: opaq flag;
Thu, 13 Jul 2000 11:36:29 +0200 wenzelm added internal, dest_internal;
Wed, 12 Jul 2000 16:44:34 +0200 wenzelm infix 'OF' is a version of 'MRS' with more appropriate argument order;
Wed, 12 Jul 2000 14:47:55 +0200 kleing about.html -> logics.html
Wed, 12 Jul 2000 14:47:34 +0200 kleing munich webserver is now sunbroy51
Wed, 12 Jul 2000 14:46:28 +0200 kleing about -> logics, better access to online libraries
Mon, 10 Jul 2000 12:17:34 +0200 paulson removal of (harmless) circular definitions
Sun, 09 Jul 2000 16:01:42 +0200 berghofe Tuned proof.
Sat, 08 Jul 2000 19:14:43 +0200 nipkow Defs are now checked for circularity (if not overloaded).
Fri, 07 Jul 2000 21:51:52 +0200 wenzelm inter_sort: keep normal!
Fri, 07 Jul 2000 18:29:34 +0200 nipkow Tightened up check of types in constant defs.
Fri, 07 Jul 2000 18:27:47 +0200 nipkow added type classes to constant's type
Fri, 07 Jul 2000 17:15:17 +0200 bauerg skp; le;
Fri, 07 Jul 2000 16:48:12 +0200 oheimb added dependency caveat
Fri, 07 Jul 2000 16:47:56 +0200 oheimb added dependency caveat
Fri, 07 Jul 2000 16:46:02 +0200 oheimb added IMP/Examples.ML dependence
Thu, 06 Jul 2000 18:12:17 +0200 wenzelm tuned msgs;
Thu, 06 Jul 2000 18:11:48 +0200 wenzelm allow comment in more commands;
Thu, 06 Jul 2000 18:11:15 +0200 wenzelm Isabelle99-1;
Thu, 06 Jul 2000 15:58:40 +0200 kleing ADD -> IAdd
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip