| 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 |