Tue, 09 Aug 2011 08:53:12 -0700 | huffman | Derivative.thy: more sensible subsection headings | changeset | files |
Tue, 09 Aug 2011 07:37:18 -0700 | huffman | Derivative.thy: clean up formatting | changeset | files |
Mon, 08 Aug 2011 21:17:52 -0700 | huffman | instance real_basis_with_inner < perfect_space | changeset | files |
Wed, 10 Aug 2011 20:53:43 +0200 | wenzelm | old term operations are legacy; | changeset | files |
Wed, 10 Aug 2011 20:12:36 +0200 | wenzelm | moved old code generator to src/Tools/; | changeset | files |
Wed, 10 Aug 2011 19:46:48 +0200 | wenzelm | avoid OldTerm operations -- with subtle changes of semantics; | changeset | files |