| Wed, 15 Nov 2006 20:50:24 +0100 | wenzelm | add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally); | changeset | files |
| Wed, 15 Nov 2006 20:50:23 +0100 | wenzelm | tuned proofs; | changeset | files |
| Wed, 15 Nov 2006 20:50:22 +0100 | wenzelm | replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected; | changeset | files |
| Wed, 15 Nov 2006 20:50:21 +0100 | wenzelm | replaced NameSpace.append by NameSpace.qualified, which handles empty names as expected; | changeset | files |
| Wed, 15 Nov 2006 17:05:48 +0100 | haftmann | dropping accidental self-imports | changeset | files |
| Wed, 15 Nov 2006 17:05:47 +0100 | haftmann | corrected polymorphism check | changeset | files |
| Wed, 15 Nov 2006 17:05:46 +0100 | haftmann | clarified code for building function equation system; explicit check of type discipline | changeset | files |
| Wed, 15 Nov 2006 17:05:45 +0100 | haftmann | moved evaluation to Code_Generator.thy | changeset | files |