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
(0) -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip