| Wed, 23 Dec 2015 14:36:45 +0100 | immler | transfer rule for bounded_linear of blinfun | changeset | files |
| Tue, 22 Dec 2015 21:58:27 +0100 | immler | theory for type of bounded linear functions; differentiation under the integral sign | changeset | files |
| Tue, 22 Dec 2015 15:39:01 +0100 | haftmann | stripped some legacy | changeset | files |
| Tue, 22 Dec 2015 15:38:59 +0100 | haftmann | tuned proofs and augmented some lemmas | changeset | files |
| Tue, 22 Dec 2015 17:41:46 +0100 | wenzelm | more standard nesting of sub-language: Parse.text allows atomic entities without quotes; | changeset | files |
| Tue, 22 Dec 2015 17:14:35 +0100 | wenzelm | proper full name within the name space of the method definition; | changeset | files |
| Tue, 22 Dec 2015 16:35:41 +0100 | wenzelm | tuned signature; | changeset | files |
| Tue, 22 Dec 2015 16:34:57 +0100 | wenzelm | isabelle update_cartouches -c -t; | changeset | files |