berghofe [Tue, 22 May 2001 15:15:16 +0200] rev 11328
Inductive characterization of wfrec combinator.
berghofe [Tue, 22 May 2001 15:12:11 +0200] rev 11327
Transitive closure is now defined via "inductive".
berghofe [Tue, 22 May 2001 15:11:43 +0200] rev 11326
Representing set for type nat is now defined via "inductive".
berghofe [Tue, 22 May 2001 15:10:06 +0200] rev 11325
Inductive definitions are now introduced earlier in the theory hierarchy.
paulson [Tue, 22 May 2001 09:26:57 +0200] rev 11324
nat_diff_split_asm, for the assumptions
paulson [Mon, 21 May 2001 14:53:30 +0200] rev 11323
if_splits and split_if_asm
paulson [Mon, 21 May 2001 14:53:11 +0200] rev 11322
fixed the X-symbol syntax for lambda
paulson [Mon, 21 May 2001 14:52:27 +0200] rev 11321
the rest of integer division
paulson [Mon, 21 May 2001 14:52:04 +0200] rev 11320
X-symbols for set theory
paulson [Mon, 21 May 2001 14:51:46 +0200] rev 11319
X-symbols for ZF