Wed, 11 Jul 2007 12:01:10 +0200 Proof terms for meta-conjunctions are now normalized before
berghofe [Wed, 11 Jul 2007 12:01:10 +0200] rev 23782
Proof terms for meta-conjunctions are now normalized before splitting up the conjunctions.
Wed, 11 Jul 2007 11:59:21 +0200 Added function norm_proof for normalizing the proof term
berghofe [Wed, 11 Jul 2007 11:59:21 +0200] rev 23781
Added function norm_proof for normalizing the proof term corresponding to a theorem.
Wed, 11 Jul 2007 11:58:40 +0200 Added function rew_proof (for pre-normalizing proofs).
berghofe [Wed, 11 Jul 2007 11:58:40 +0200] rev 23780
Added function rew_proof (for pre-normalizing proofs).
Wed, 11 Jul 2007 11:56:59 +0200 Function unify_consts moved from OldInductivePackage to PrimrecPackage.
berghofe [Wed, 11 Jul 2007 11:56:59 +0200] rev 23779
Function unify_consts moved from OldInductivePackage to PrimrecPackage.
Wed, 11 Jul 2007 11:54:21 +0200 Adapted to new inductive definition package.
berghofe [Wed, 11 Jul 2007 11:54:21 +0200] rev 23778
Adapted to new inductive definition package.
Wed, 11 Jul 2007 11:54:03 +0200 Renamed accessible part for predicates to accp.
berghofe [Wed, 11 Jul 2007 11:54:03 +0200] rev 23777
Renamed accessible part for predicates to accp.
Wed, 11 Jul 2007 11:52:45 +0200 renamed inductive2 to inductive.
berghofe [Wed, 11 Jul 2007 11:52:45 +0200] rev 23776
renamed inductive2 to inductive.
Wed, 11 Jul 2007 11:52:28 +0200 Renamed inductive2 to inductive.
berghofe [Wed, 11 Jul 2007 11:52:28 +0200] rev 23775
Renamed inductive2 to inductive.
Wed, 11 Jul 2007 11:52:00 +0200 Hide member constant.
berghofe [Wed, 11 Jul 2007 11:52:00 +0200] rev 23774
Hide member constant.
Wed, 11 Jul 2007 11:51:15 +0200 Reverted renaming of "member".
berghofe [Wed, 11 Jul 2007 11:51:15 +0200] rev 23773
Reverted renaming of "member".
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip