Skip to content
Success

Changes

Summary

  1. clarified settings -- avoid hard-wired directories; tuned documentation;
  2. example for Types_To_Sets: transfer from type-based linear algebra to subspaces
  3. added lemmas and transfer rules
Changeset 68523:ccacc84e0251 by wenzelm:
clarified settings -- avoid hard-wired directories;<br>tuned documentation;
The file was modified NEWS (diff)
The file was modified etc/settings (diff)
The file was modified src/Doc/System/Environment.thy (diff)
The file was modified src/Doc/System/Server.thy (diff)
The file was modified src/Doc/System/Sessions.thy (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 68522:d9cbc1e8644d by immler:
example for Types_To_Sets: transfer from type-based linear algebra to subspaces
The file was addedsrc/HOL/Types_To_Sets/Examples/Group_On_With.thy
The file was addedsrc/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
The file was addedsrc/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 68521:1bad08165162 by immler:
added lemmas and transfer rules
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Lifting_Set.thy (diff)
The file was modified src/HOL/Transfer.thy (diff)