Sat, 09 Jun 2001 14:22:08 +0200 wenzelm tuned
Sat, 09 Jun 2001 14:18:19 +0200 wenzelm tuned Primes theory;
Sat, 09 Jun 2001 08:44:04 +0200 paulson addition of the GREATEST quantifier
Sat, 09 Jun 2001 08:43:38 +0200 paulson renaming of evs in the Fake rule
Sat, 09 Jun 2001 08:42:29 +0200 paulson new material from the Sylow proof
Sat, 09 Jun 2001 08:42:06 +0200 paulson simplified a proof using new dvd rules
Sat, 09 Jun 2001 08:41:25 +0200 paulson moved Primes.thy from NumberTheory to Library
Fri, 08 Jun 2001 08:50:08 +0200 nipkow Removed BCV
Tue, 05 Jun 2001 09:51:04 +0200 nipkow *** empty log message ***
Tue, 05 Jun 2001 09:41:11 +0200 nipkow This is now superseded by MicroJava/BV
Fri, 01 Jun 2001 11:04:19 +0200 paulson renamed # to ## to avoid clashing with List cons
Fri, 01 Jun 2001 11:03:50 +0200 paulson now checks for leading meta-quantifiers and complains, instead of
Thu, 31 May 2001 22:34:58 +0200 wenzelm tuned
Thu, 31 May 2001 20:53:49 +0200 wenzelm added HOL-CTL;
Thu, 31 May 2001 20:52:51 +0200 wenzelm tuned
Thu, 31 May 2001 18:28:23 +0200 paulson examples files start from Main instead of various ZF theories
Thu, 31 May 2001 17:57:02 +0200 wenzelm invent_names
Thu, 31 May 2001 17:24:56 +0200 bauerg added HOL-CTL example;
Thu, 31 May 2001 17:06:00 +0200 oheimb added Library/Nat_Infinity.thy and Library/Continuity.thy
Thu, 31 May 2001 16:53:00 +0200 oheimb added FOCUS including the One-Element Buffer by Manfred Broy
Thu, 31 May 2001 16:52:54 +0200 oheimb added Library/Nat_Infinity.thy and Library/Continuity.thy
Thu, 31 May 2001 16:52:47 +0200 oheimb added stream length, map, and filter
Thu, 31 May 2001 16:52:35 +0200 oheimb corrected ML names of definitions, added chain_shift
Thu, 31 May 2001 16:52:32 +0200 oheimb corrected ML names of definitions
Thu, 31 May 2001 16:52:20 +0200 oheimb improved iff_add_global, new function add_rules factoring out common behaviour
Thu, 31 May 2001 16:52:02 +0200 oheimb streamlined addIffs/delIffs, added warnings
Thu, 31 May 2001 16:51:26 +0200 oheimb replaced Sel_injective_cprod by new injective_fst_snd
Thu, 31 May 2001 16:51:14 +0200 oheimb added lub_range_mono and lub_range_shift
Thu, 31 May 2001 16:50:17 +0200 oheimb added chain_monofun
Thu, 31 May 2001 16:50:16 +0200 oheimb added same_fstI as safe intro rule
Thu, 31 May 2001 16:50:15 +0200 oheimb added injective_fst_snd
Thu, 31 May 2001 16:50:14 +0200 oheimb added nat_not_singleton (also to simpset)
Thu, 31 May 2001 16:50:13 +0200 oheimb added Least_Suc2
Thu, 31 May 2001 16:50:04 +0200 oheimb added list_all2_trans
Thu, 31 May 2001 16:17:28 +0200 oheimb added weak_coinduct_image
Thu, 31 May 2001 16:07:35 +0200 nipkow Allow Suc-numerals as coefficients in lin-arith formulae
Thu, 31 May 2001 12:43:56 +0200 oheimb corrected entry for iff attribute
Wed, 30 May 2001 18:54:10 +0200 oheimb extended doc for iff attribute
Wed, 30 May 2001 10:48:59 +0200 bauerg injectivity of ^;
Tue, 29 May 2001 11:43:12 +0200 paulson deleted a needless reference to rtrancl_unfold
Mon, 28 May 2001 18:48:28 +0200 oheimb improved handling of space before/after parentheses
Tue, 22 May 2001 15:15:16 +0200 berghofe Inductive characterization of wfrec combinator.
Tue, 22 May 2001 15:12:11 +0200 berghofe Transitive closure is now defined via "inductive".
Tue, 22 May 2001 15:11:43 +0200 berghofe Representing set for type nat is now defined via "inductive".
Tue, 22 May 2001 15:10:06 +0200 berghofe Inductive definitions are now introduced earlier in the theory hierarchy.
Tue, 22 May 2001 09:26:57 +0200 paulson nat_diff_split_asm, for the assumptions
Mon, 21 May 2001 14:53:30 +0200 paulson if_splits and split_if_asm
Mon, 21 May 2001 14:53:11 +0200 paulson fixed the X-symbol syntax for lambda
Mon, 21 May 2001 14:52:27 +0200 paulson the rest of integer division
Mon, 21 May 2001 14:52:04 +0200 paulson X-symbols for set theory
Mon, 21 May 2001 14:51:46 +0200 paulson X-symbols for ZF
Mon, 21 May 2001 14:46:30 +0200 paulson X-symbols for ZF
Mon, 21 May 2001 14:45:52 +0200 paulson X-symbols for set theory
Mon, 21 May 2001 14:36:24 +0200 paulson X-symbols for set theory
Mon, 21 May 2001 14:35:54 +0200 paulson Division examples
Mon, 21 May 2001 12:51:15 +0200 paulson ZF: division
Sun, 20 May 2001 13:16:27 +0200 paulson new theorem dvd_mult_right
Sun, 20 May 2001 11:20:41 +0200 nipkow added (no)_type_brackets
Sat, 19 May 2001 12:21:34 +0200 paulson power_le_dvd replaces power_less_dvd
Sat, 19 May 2001 12:19:23 +0200 paulson spelling check
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip