Summary
- more uniform use of Reconstruct.clean_proof_of;
- clarified message: print subgoal number instead of potentially large term;
- tuned;
- suppress warnings uniformly, even in explicit commands 'find_theorems', 'solve_direct';
- tuned;
The file was modified | NEWS (diff) |
The file was modified | src/HOL/Proofs/ex/Proof_Terms.thy (diff) |
The file was modified | src/HOL/Proofs/ex/XML_Data.thy (diff) |
The file was modified | src/Pure/Isar/isar_cmd.ML (diff) |
The file was modified | src/Pure/Proof/proof_syntax.ML (diff) |
The file was modified | src/Pure/Proof/reconstruct.ML (diff) |
The file was modified | src/Pure/Thy/thy_output.ML (diff) |
The file was modified | src/Tools/solve_direct.ML (diff) |
The file was modified | src/Pure/Tools/find_theorems.ML (diff) |
The file was modified | src/Tools/solve_direct.ML (diff) |
The file was modified | src/Pure/Tools/find_theorems.ML (diff) |
The file was modified | src/Tools/solve_direct.ML (diff) |
The file was modified | src/Tools/solve_direct.ML (diff) |