| Thu, 26 May 2016 15:27:50 +0200 | haftmann | corrected closure scope of static_conv_thingol; | changeset | files |
| Thu, 26 May 2016 15:27:50 +0200 | haftmann | clarified proof context vs. background theory | changeset | files |
| Thu, 26 May 2016 15:27:50 +0200 | haftmann | explicit quasi-global context for nbe conversions -- works around quasi-global type variable handling in lift_triv_classes_conv | changeset | files |