Summary
- merged
- Modified transfer principle in HOL/NSA to cause less ho-unficiation
The file was modified | src/HOL/Nonstandard_Analysis/StarDef.thy (diff) |
The file was modified | src/HOL/Nonstandard_Analysis/transfer.ML (diff) |
The file was modified | src/HOL/Nonstandard_Analysis/StarDef.thy (diff) |
The file was modified | src/HOL/Nonstandard_Analysis/transfer.ML (diff) |