2000-05-24 paulson 2000-05-24 installing the plus_ac0 axclass
2000-05-24 paulson 2000-05-24 Adding SetInterval, deleting UNITY/LessThan
2000-05-24 paulson 2000-05-24 added parent
2000-05-24 paulson 2000-05-24 facts about lessThan, etc., mostly from UNITY/LessThan
2000-05-24 paulson 2000-05-24 installing the plus_ac0 simprules
2000-05-24 paulson 2000-05-24 rewrote a very long proof (Key_analz_image_Key) because it had stopped working
2000-05-24 paulson 2000-05-24 overloaded 0
2000-05-24 paulson 2000-05-24 tidying for overloaded 0, setsum, etc.
2000-05-24 paulson 2000-05-24 installing plus_ac0 for multisets
2000-05-24 paulson 2000-05-24 replacing "below" by "lessThan"
2000-05-24 paulson 2000-05-24 installing plus_ac0 for int
2000-05-24 paulson 2000-05-24 restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
2000-05-24 wenzelm 2000-05-24 tuned;
2000-05-24 wenzelm 2000-05-24 "done" command;
2000-05-24 wenzelm 2000-05-24 fixed index;
2000-05-24 paulson 2000-05-24 restored NatSum.thy
2000-05-23 paulson 2000-05-23 now 0 is overloaded
2000-05-23 paulson 2000-05-23 added type constraint ::nat because 0 is now overloaded
2000-05-23 paulson 2000-05-23 IntRingDefs is now redundant
2000-05-23 paulson 2000-05-23 new type class "zero" so that 0 can be overloaded
2000-05-23 paulson 2000-05-23 finally sum_below is overloaded properly
2000-05-23 paulson 2000-05-23 Multisets have a zero: the empty multiset
2000-05-23 paulson 2000-05-23 defining 0::int to be (int 0)
2000-05-23 paulson 2000-05-23 Now that 0 is overloaded, constant "zero" and its type class "zero" are no longer needed. Also IntRingDefs is redundant
2000-05-23 paulson 2000-05-23 added type constraint ::nat because 0 is now overloaded
2000-05-23 paulson 2000-05-23 theory file NatSum.thy no longer needed new files for the Allocator: AllocBase.{thy,ML}
2000-05-23 paulson 2000-05-23 theory file NatSum.thy no longer needed
2000-05-23 paulson 2000-05-23 Sums of geometric series
2000-05-23 paulson 2000-05-23 use of AllocBase
2000-05-23 paulson 2000-05-23 removal of lessThan; use of AllocBase
2000-05-23 paulson 2000-05-23 declared sum_below
2000-05-23 paulson 2000-05-23 new files for the Allocator
2000-05-23 paulson 2000-05-23 eta-expanded to handle value polymorphism
2000-05-23 wenzelm 2000-05-23 improved warning messages;
2000-05-23 nipkow 2000-05-23 SetInterval
2000-05-23 nipkow 2000-05-23 Added SetInterval
2000-05-22 wenzelm 2000-05-22 new Isar version of HOL-AxClasses-Tutorial;
2000-05-22 wenzelm 2000-05-22 tuned;
2000-05-22 wenzelm 2000-05-22 * Pure: changed syntax of local blocks from {{ }} to { }; * Pure: syntax of sorts made inner, i.e. have to write "{a, b, c}";
2000-05-22 wenzelm 2000-05-22 new Isar version;
2000-05-22 paulson 2000-05-22 tidied and made to work with AddSIs [psubsetI]
2000-05-22 paulson 2000-05-22 further tidying
2000-05-22 paulson 2000-05-22 loading the new theory MultisetOrder
2000-05-22 paulson 2000-05-22 multisets are partially ordered
2000-05-22 paulson 2000-05-22 Proving that multisets are partially ordered New infix syntax for element-hood
2000-05-22 paulson 2000-05-22 Proving that multisets are partially ordered New infix syntax for element-hood New theorem size_union
2000-05-22 paulson 2000-05-22 psubsetI is a safe rule
2000-05-22 paulson 2000-05-22 new file Induct/MultisetOrder.thy
2000-05-22 paulson 2000-05-22 fold_commute, fold_nest_Un_Int, setsum_Un and other new results
2000-05-22 wenzelm 2000-05-22 tuned;
2000-05-22 wenzelm 2000-05-22 added NatClass;
2000-05-22 wenzelm 2000-05-22 show_consts no longer requires show_types;
2000-05-22 wenzelm 2000-05-22 tuned;
2000-05-22 wenzelm 2000-05-22 tuned;
2000-05-22 wenzelm 2000-05-22 obsolete;
2000-05-21 wenzelm 2000-05-21 added notes;
2000-05-21 wenzelm 2000-05-21 new Isar version;
2000-05-21 wenzelm 2000-05-21 replaced {{ }} by { };
2000-05-21 wenzelm 2000-05-21 cite isabelle-axclass;
2000-05-21 wenzelm 2000-05-21 improved \BG, \EN;