Tue, 17 Dec 2002 11:04:58 +0100 paulson new int induction rules
Tue, 17 Dec 2002 11:04:30 +0100 paulson new material for trace_unify_fail
Mon, 16 Dec 2002 13:43:11 +0100 berghofe Added mk_int and mk_list.
Mon, 16 Dec 2002 11:18:35 +0100 berghofe Code generator for datatypes now also generates suitable term_of functions (when
Mon, 16 Dec 2002 11:17:16 +0100 berghofe - Added mode reference variable (may be used to switch on and off specific
Fri, 13 Dec 2002 18:14:25 +0100 oheimb cent/currency: changed from wasysym to textcomp because of PDF problems
Fri, 13 Dec 2002 16:49:08 +0100 paulson trace_unify_fail
Fri, 13 Dec 2002 16:48:20 +0100 paulson integer induction rules
Fri, 13 Dec 2002 14:20:47 +0100 berghofe size_of_proof no longer includes size_of_term
Fri, 13 Dec 2002 13:47:13 +0100 paulson deleted redundant line
Thu, 12 Dec 2002 11:38:18 +0100 paulson Better treatment of equality in premises of inductive definitions. Less
Thu, 12 Dec 2002 11:33:48 +0100 ballarin Fixed error that affected document preperation.
Wed, 11 Dec 2002 10:12:48 +0100 ballarin HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
Tue, 10 Dec 2002 10:40:32 +0100 berghofe Added size_of_proof.
Mon, 09 Dec 2002 10:38:56 +0100 ballarin Fixed bug in simpdata.ML that prevented the use of congruence rules from a
(0) -10000 -3000 -1000 -300 -100 -15 +15 +100 +300 +1000 +3000 +10000 +30000 tip