Summary
- clarified antiquotations;
- tuned;
- minor performance tuning;
The file was modified | src/HOL/Tools/Argo/argo_tactic.ML (diff) |
The file was modified | src/HOL/Tools/Argo/argo_tactic.ML (diff) |
The file was modified | src/Pure/thm.ML (diff) |
The file was modified | src/HOL/Tools/Argo/argo_tactic.ML (diff) |
The file was modified | src/HOL/Tools/Argo/argo_tactic.ML (diff) |
The file was modified | src/Pure/thm.ML (diff) |