src/HOL/NumberTheory/Chinese.thy
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Wed, 30 Aug 2006 03:19:08 +0200 webertj lin_arith_prover: splitting reverted because of performance loss
Mon, 31 Jul 2006 21:06:40 +0200 webertj lin_arith_prover splits certain operators (e.g. min, max, abs)
Wed, 17 May 2006 01:23:41 +0200 wenzelm prefer 'definition' over low-level defs;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Mon, 11 Oct 2004 07:42:22 +0200 nipkow Proofs needed to be updated because induction now preserves name of
Fri, 10 Sep 2004 20:04:14 +0200 nipkow Added antisymmetry simproc
Mon, 12 Jan 2004 16:51:45 +0100 paulson Added lemmas to Ring_and_Field with slightly modified simplification rules
Tue, 27 Aug 2002 11:03:05 +0200 wenzelm *** empty log message ***
Thu, 30 May 2002 10:12:52 +0200 nipkow Modifications due to enhanced linear arithmetic.
Mon, 22 Oct 2001 11:54:22 +0200 paulson Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
Fri, 05 Oct 2001 21:52:39 +0200 wenzelm sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
Tue, 07 Aug 2001 16:36:52 +0200 paulson Tweaks for 1 -> 1'
Sun, 04 Feb 2001 19:31:13 +0100 wenzelm HOL-NumberTheory: converted to new-style format and proper document setup;
Thu, 03 Aug 2000 10:46:01 +0200 paulson Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
less more (0) tip