Fri, 18 May 2007 16:13:07 +0200 | huffman | avoid using real_mult_inverse_left; cleaned up | file | diff | annotate |
Thu, 17 May 2007 21:51:32 +0200 | huffman | avoid using redundant lemmas from RealDef.thy | file | diff | annotate |
Fri, 17 Nov 2006 02:20:03 +0100 | wenzelm | more robust syntax for definition/abbreviation/notation; | file | diff | annotate |
Tue, 07 Nov 2006 11:47:57 +0100 | wenzelm | renamed 'const_syntax' to 'notation'; | 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 |
Sun, 11 Jun 2006 22:45:53 +0200 | wenzelm | fixed subst step; | file | diff | annotate |
Fri, 02 Jun 2006 23:22:29 +0200 | wenzelm | misc cleanup; | file | diff | annotate |