Skip to content
Success

Changes

Summary

  1. misc tuning and modernization;
  2. isabelle update_cartouches -c -t;
  3. misc tuning and modernization;
  4. new lemma
  5. more explicit Argo proof traces; more correct proof replay for term applications
Changeset 66305:7454317f883c by wenzelm:
misc tuning and modernization;
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)
Changeset 66304:cde6ceffcbc7 by wenzelm:
isabelle update_cartouches -c -t;
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)
Changeset 66303:210dae34b8bc by wenzelm:
misc tuning and modernization;
The file was modified src/HOL/ex/Classical.thy (diff)
Changeset 66302:fd89f97c80c2 by nipkow:
new lemma
The file was modified src/HOL/Data_Structures/Tree23.thy (diff)
Changeset 66301:8a6a89d6cf2b by boehmes:
more explicit Argo proof traces; more correct proof replay for term applications
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)