Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);
  2. tuned;
  3. uniform standard_vars for terms and proof terms;
  4. treat simproc results as atomic -- more compact proof terms;
Changeset 70531:2d2b5a8e8d59 by wenzelm:
clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70530:81a8eba6639c by wenzelm:
tuned;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70529:2ecbbe6b35db by wenzelm:
uniform standard_vars for terms and proof terms;
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70528:9b3610fe74d6 by wenzelm:
treat simproc results as atomic -- more compact proof terms;
The file was modified src/Pure/raw_simplifier.ML (diff)