Summary
- clarified settings -- avoid hard-wired directories; tuned documentation;
- example for Types_To_Sets: transfer from type-based linear algebra to subspaces
- added lemmas and transfer rules
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) |
The file was added | src/HOL/Types_To_Sets/Examples/Group_On_With.thy |
The file was added | src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy |
The file was added | src/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) |
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) |