| Mon, 26 Aug 2013 16:13:20 +0200 | wenzelm | prefer Binding.name_of over Binding.print -- the latter leads to funny quotes and markup within the constructed term; | changeset | files |
| Mon, 26 Aug 2013 15:57:09 +0200 | wenzelm | always transfer thm where attributes are applied -- relevant for internal 'notes' (e.g. via bundle 'includes') in contrast to external 'notes' (cf. Proof_Context.retrieve_thms); | changeset | files |
| Mon, 26 Aug 2013 15:45:51 +0200 | wenzelm | proper context; | changeset | files |