Wed, 19 Dec 2001 00:26:04 +0100 wenzelm tuned;
Tue, 18 Dec 2001 21:28:01 +0100 kleing removed preallocated heaps axiom (now in type safety invariant)
Tue, 18 Dec 2001 18:37:56 +0100 wenzelm updated;
Tue, 18 Dec 2001 18:06:10 +0100 paulson New type definition diagram
Tue, 18 Dec 2001 17:31:08 +0100 nipkow added exec_lub
Tue, 18 Dec 2001 17:15:41 +0100 paulson new type definition figure
Tue, 18 Dec 2001 16:44:00 +0100 paulson minor suggestions from Markus
Tue, 18 Dec 2001 16:14:56 +0100 paulson additional material
Tue, 18 Dec 2001 16:14:50 +0100 wenzelm * system: tested support for MacOS X;
Tue, 18 Dec 2001 15:04:19 +0100 paulson better simplification makes steps redundant
Tue, 18 Dec 2001 15:03:27 +0100 paulson replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll
Tue, 18 Dec 2001 14:27:57 +0100 wenzelm tuned;
Tue, 18 Dec 2001 14:20:38 +0100 wenzelm use Locale.read/cert_context_statement;
Tue, 18 Dec 2001 13:15:21 +0100 nipkow *** empty log message ***
Tue, 18 Dec 2001 02:22:27 +0100 wenzelm tuned;
Tue, 18 Dec 2001 02:20:23 +0100 wenzelm improved mixfix_args;
Tue, 18 Dec 2001 02:20:02 +0100 wenzelm tuned Type.unify;
Tue, 18 Dec 2001 02:19:31 +0100 wenzelm simultaneous type-inference of complete context/statement specifications;
Tue, 18 Dec 2001 02:18:38 +0100 wenzelm tuned interface of unify, param;
Tue, 18 Dec 2001 02:17:20 +0100 wenzelm tuned Type.unify;
Mon, 17 Dec 2001 14:27:18 +0100 nipkow mods due to changed 1-point simprocs (quantifier1).
Mon, 17 Dec 2001 14:24:11 +0100 nipkow mods due to improved 1-point simprocs (quantifier1).
Mon, 17 Dec 2001 14:23:10 +0100 nipkow mods due to mor powerful simprocs for 1-point rules (quantifier1).
Mon, 17 Dec 2001 14:21:59 +0100 nipkow now permutations of quantifiers are allowed as well.
Mon, 17 Dec 2001 13:25:18 +0100 kleing fixed JVMListExample
Sun, 16 Dec 2001 00:20:17 +0100 kleing MicroJava exception merge
Sun, 16 Dec 2001 00:19:54 +0100 kleing temporarily removed JVMListExample
Sun, 16 Dec 2001 00:19:08 +0100 kleing exception merge + cleanup
Sun, 16 Dec 2001 00:18:44 +0100 kleing exception merge, doesn't work yet
Sun, 16 Dec 2001 00:18:17 +0100 kleing exception merge, cleanup, tuned
Sun, 16 Dec 2001 00:17:44 +0100 kleing exceptions
Sun, 16 Dec 2001 00:17:18 +0100 kleing list_all2_rev
Fri, 14 Dec 2001 22:32:52 +0100 wenzelm removed debug stuff;
Fri, 14 Dec 2001 22:30:54 +0100 wenzelm support for ``indexed syntax'' (using "\<index>" argument instead of "_");
Fri, 14 Dec 2001 22:29:51 +0100 wenzelm removed special treatment of "_" in syntax (now covered by \<index> arg);
Fri, 14 Dec 2001 22:29:11 +0100 wenzelm tuned locale interface;
Fri, 14 Dec 2001 22:28:52 +0100 wenzelm proper treatment of internal parameters;
Fri, 14 Dec 2001 22:28:13 +0100 wenzelm \usepackage[latin1]{inputenc};
Fri, 14 Dec 2001 22:27:58 +0100 wenzelm Wenzel:2001:Isar-examples;
Fri, 14 Dec 2001 22:27:43 +0100 wenzelm updated;
Fri, 14 Dec 2001 22:27:20 +0100 wenzelm mixfix syntax for selectors;
Fri, 14 Dec 2001 22:26:55 +0100 wenzelm record: mixfix;
Fri, 14 Dec 2001 11:57:03 +0100 wenzelm export used_types;
Fri, 14 Dec 2001 11:56:09 +0100 wenzelm Locale.activate_context;
Fri, 14 Dec 2001 11:55:34 +0100 wenzelm beginning support for type instantiation;
Fri, 14 Dec 2001 11:54:47 +0100 wenzelm varify returns newly introduced variables;
Fri, 14 Dec 2001 11:54:13 +0100 wenzelm varifyT' returns newly introduces variables;
Fri, 14 Dec 2001 11:53:31 +0100 wenzelm added invent_type_names;
Fri, 14 Dec 2001 11:52:54 +0100 wenzelm changed Thm.varifyT';
Fri, 14 Dec 2001 11:52:32 +0100 wenzelm type_env;
Fri, 14 Dec 2001 11:51:52 +0100 wenzelm added type_env function;
Fri, 14 Dec 2001 11:51:01 +0100 wenzelm export add_tvarsT etc.;
Fri, 14 Dec 2001 11:50:38 +0100 wenzelm changed Type.varify;
Fri, 14 Dec 2001 11:50:19 +0100 wenzelm Term.invent_type_names;
Thu, 13 Dec 2001 19:05:10 +0100 nipkow *** empty log message ***
Thu, 13 Dec 2001 17:57:55 +0100 nipkow *** empty log message ***
Thu, 13 Dec 2001 17:44:56 +0100 wenzelm made SML/XL happy;
Thu, 13 Dec 2001 16:48:34 +0100 nipkow *** empty log message ***
Thu, 13 Dec 2001 16:48:07 +0100 nipkow Terminator now uses arith_tac as well.
Thu, 13 Dec 2001 16:47:35 +0100 nipkow comp -> rel_comp
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip