src/HOL/MicroJava/Comp/CorrCompTp.thy
Thu, 12 Nov 2009 17:21:51 +0100 hoelzl Remove map_compose, replaced by map_map
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Tue, 22 Sep 2009 15:36:55 +0200 haftmann be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
Fri, 28 Aug 2009 20:18:33 +0200 nipkow tuned proofs
Fri, 28 Aug 2009 18:52:41 +0200 nipkow Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
Sat, 09 May 2009 09:17:29 +0200 haftmann interface changes in linarith.ML
Wed, 04 Mar 2009 10:47:20 +0100 nipkow Made Option a separate theory and renamed option_map to Option.map
Wed, 01 Aug 2007 16:55:37 +0200 wenzelm tuned config options: eliminated separate attribute "option";
Tue, 31 Jul 2007 00:56:31 +0200 wenzelm turned fast_arith_split/neq_limit into configuration options;
Mon, 11 Jun 2007 11:06:04 +0200 chaieb tuned Proof
Sat, 19 May 2007 11:33:26 +0200 haftmann added qualification for ambiguous definition names
Tue, 24 Apr 2007 15:15:52 +0200 berghofe Adapted to new parse translation for case expressions.
Sun, 12 Nov 2006 19:22:10 +0100 nipkow started reorgnization of lattice theories
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)
less more (0) -15 tip