Changes

Summary

merged
more abstract naming
tuned
workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar

Changeset 68432:6f3bd27ba389 by nipkow: merged
Changeset 68431:b294e095f64c by nipkow: more abstract naming
The file was modified	`src/HOL/Data_Structures/AA_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AA_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AVL_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AVL_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Brother12_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Brother12_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Map_Specs.thy` (diff)
The file was modified	`src/HOL/Data_Structures/RBT_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/RBT_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree234_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree234_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree23_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree23_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree_Set.thy` (diff)
Changeset 68430:b0eb6a91924d by immler: tuned
The file was modified	`src/HOL/Types_To_Sets/unoverload_type.ML` (diff)
Changeset 68429:38961724a017 by immler: workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
The file was modified	`src/HOL/Types_To_Sets/unoverload_type.ML` (diff)