Fri, 09 May 2014 08:13:36 +0200 | haftmann | modernized setups | changeset | files |
Fri, 09 May 2014 08:13:36 +0200 | haftmann | degeneralized value command into HOL | changeset | files |
Fri, 09 May 2014 08:13:36 +0200 | haftmann | dimiss simplified as evaluator due to little practical relevance | changeset | files |
Fri, 09 May 2014 08:13:36 +0200 | haftmann | prefer separate command for approximation | changeset | files |
Fri, 09 May 2014 08:13:36 +0200 | haftmann | removed junk from library theory | changeset | files |
Fri, 09 May 2014 08:13:28 +0200 | haftmann | note of_class rule for type classes in theory: useful to promote class instance proofs to locale interpretation proofs | changeset | files |