Tue, 07 Nov 2006 19:40:13 +0100 | wenzelm | tuned specifications; | file | diff | annotate |
Mon, 09 Oct 2006 02:19:51 +0200 | wenzelm | attribute symmetric: zero_var_indexes; | file | diff | annotate |
Mon, 31 Jul 2006 21:06:40 +0200 | webertj | lin_arith_prover splits certain operators (e.g. min, max, abs) | file | diff | annotate |
Wed, 26 Jul 2006 19:23:04 +0200 | webertj | linear arithmetic splits certain operators (e.g. min, max, abs) | file | diff | annotate |
Thu, 08 Dec 2005 12:50:04 +0100 | wenzelm | tuned sources and proofs | file | diff | annotate |
Tue, 12 Jul 2005 17:56:03 +0200 | avigad | added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) | file | diff | annotate |
Thu, 07 Jul 2005 12:39:17 +0200 | nipkow | linear arithmetic now takes "&" in assumptions apart. | file | diff | annotate |