Summary
- misc tuning and modernization;
- isabelle update_cartouches -c -t;
- misc tuning and modernization;
- new lemma
- more explicit Argo proof traces; more correct proof replay for term applications
The file was modified | src/HOL/Number_Theory/Pocklington.thy (diff) |
The file was modified | src/HOL/Number_Theory/Residues.thy (diff) |
The file was modified | src/HOL/Number_Theory/Totient.thy (diff) |
The file was modified | src/HOL/Analysis/Improper_Integral.thy (diff) |
The file was modified | src/HOL/Analysis/Topology_Euclidean_Space.thy (diff) |
The file was modified | src/HOL/Analysis/Winding_Numbers.thy (diff) |
The file was modified | src/HOL/Number_Theory/Residues.thy (diff) |
The file was modified | src/HOL/ex/Classical.thy (diff) |
The file was modified | src/HOL/Data_Structures/Tree23.thy (diff) |
The file was modified | src/HOL/Tools/Argo/argo_tactic.ML (diff) |
The file was modified | src/HOL/ex/Argo_Examples.thy (diff) |
The file was modified | src/Tools/Argo/argo_expr.ML (diff) |
The file was modified | src/Tools/Argo/argo_proof.ML (diff) |
The file was modified | src/Tools/Argo/argo_rewr.ML (diff) |