Wed, 24 May 2000 18:41:49 +0200 paulson replacing "below" by "lessThan"
Wed, 24 May 2000 18:41:09 +0200 paulson installing plus_ac0 for int
Wed, 24 May 2000 18:40:01 +0200 paulson restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
Wed, 24 May 2000 18:19:04 +0200 wenzelm tuned;
Wed, 24 May 2000 18:04:20 +0200 wenzelm "done" command;
Wed, 24 May 2000 13:16:01 +0200 wenzelm fixed index;
Wed, 24 May 2000 12:21:26 +0200 paulson restored NatSum.thy
Tue, 23 May 2000 18:29:17 +0200 paulson now 0 is overloaded
Tue, 23 May 2000 18:28:11 +0200 paulson added type constraint ::nat because 0 is now overloaded
Tue, 23 May 2000 18:24:48 +0200 paulson IntRingDefs is now redundant
Tue, 23 May 2000 18:22:19 +0200 paulson new type class "zero" so that 0 can be overloaded
Tue, 23 May 2000 18:21:51 +0200 paulson finally sum_below is overloaded properly
Tue, 23 May 2000 18:19:06 +0200 paulson Multisets have a zero: the empty multiset
Tue, 23 May 2000 18:14:57 +0200 paulson defining 0::int to be (int 0)
Tue, 23 May 2000 18:08:52 +0200 paulson Now that 0 is overloaded, constant "zero" and its type class "zero" are
Tue, 23 May 2000 18:06:22 +0200 paulson added type constraint ::nat because 0 is now overloaded
Tue, 23 May 2000 12:44:03 +0200 paulson theory file NatSum.thy no longer needed
Tue, 23 May 2000 12:36:36 +0200 paulson theory file NatSum.thy no longer needed
Tue, 23 May 2000 12:35:57 +0200 paulson Sums of geometric series
Tue, 23 May 2000 12:35:18 +0200 paulson use of AllocBase
Tue, 23 May 2000 12:34:26 +0200 paulson removal of lessThan; use of AllocBase
Tue, 23 May 2000 12:32:24 +0200 paulson declared sum_below
Tue, 23 May 2000 12:31:38 +0200 paulson new files for the Allocator
Tue, 23 May 2000 12:30:29 +0200 paulson eta-expanded to handle value polymorphism
Tue, 23 May 2000 12:13:45 +0200 wenzelm improved warning messages;
Tue, 23 May 2000 09:08:18 +0200 nipkow SetInterval
Tue, 23 May 2000 07:32:24 +0200 nipkow Added SetInterval
Mon, 22 May 2000 16:05:22 +0200 wenzelm new Isar version of HOL-AxClasses-Tutorial;
Mon, 22 May 2000 16:04:32 +0200 wenzelm tuned;
Mon, 22 May 2000 16:03:43 +0200 wenzelm * Pure: changed syntax of local blocks from {{ }} to { };
Mon, 22 May 2000 13:29:21 +0200 wenzelm new Isar version;
Mon, 22 May 2000 13:20:47 +0200 paulson tidied and made to work with AddSIs [psubsetI]
Mon, 22 May 2000 13:19:20 +0200 paulson further tidying
Mon, 22 May 2000 12:35:34 +0200 paulson loading the new theory MultisetOrder
Mon, 22 May 2000 12:35:02 +0200 paulson multisets are partially ordered
Mon, 22 May 2000 12:30:40 +0200 paulson Proving that multisets are partially ordered
Mon, 22 May 2000 12:30:07 +0200 paulson Proving that multisets are partially ordered
Mon, 22 May 2000 12:29:02 +0200 paulson psubsetI is a safe rule
Mon, 22 May 2000 12:28:34 +0200 paulson new file Induct/MultisetOrder.thy
Mon, 22 May 2000 12:27:11 +0200 paulson fold_commute, fold_nest_Un_Int, setsum_Un and other new results
Mon, 22 May 2000 12:05:23 +0200 wenzelm tuned;
Mon, 22 May 2000 12:05:12 +0200 wenzelm added NatClass;
Mon, 22 May 2000 11:57:27 +0200 wenzelm show_consts no longer requires show_types;
Mon, 22 May 2000 11:56:55 +0200 wenzelm tuned;
Mon, 22 May 2000 10:31:44 +0200 wenzelm tuned;
Mon, 22 May 2000 10:02:58 +0200 wenzelm obsolete;
Sun, 21 May 2000 21:49:06 +0200 wenzelm added notes;
Sun, 21 May 2000 21:48:39 +0200 wenzelm new Isar version;
Sun, 21 May 2000 14:49:28 +0200 wenzelm replaced {{ }} by { };
Sun, 21 May 2000 14:44:01 +0200 wenzelm cite isabelle-axclass;
Sun, 21 May 2000 14:42:35 +0200 wenzelm improved \BG, \EN;
Sun, 21 May 2000 14:37:17 +0200 wenzelm removed is_type_abbr;
Sun, 21 May 2000 14:36:29 +0200 wenzelm removed is_type_abbr;
Sun, 21 May 2000 14:35:27 +0200 wenzelm adapted to inner syntax of sorts;
Sun, 21 May 2000 14:33:46 +0200 wenzelm replaced {{ }} by { };
Sun, 21 May 2000 14:32:47 +0200 wenzelm added sort_of_term;
Sun, 21 May 2000 14:31:41 +0200 wenzelm added read_sort;
Sun, 21 May 2000 01:18:29 +0200 wenzelm *** empty log message ***
Sun, 21 May 2000 01:17:12 +0200 wenzelm new stuff;
Sun, 21 May 2000 01:16:54 +0200 wenzelm \urlstyle{rm};
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip