Changes

Summary

qualify interpretations to avoid clashes
more abstract names
tuned exception
restructured
result of unoverload is not in normal form
tuned
allow for a list of vars
parse var

Changeset 68440:6826718f732d by nipkow: qualify interpretations to avoid clashes
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/RBT_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/RBT_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Set_Specs.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 68439:c8101022e52a by nipkow: more abstract names
The file was modified	`src/HOL/Data_Structures/Set_Specs.thy` (diff)
Changeset 68438:f04d0e75e439 by immler: tuned exception
The file was modified	`src/HOL/Types_To_Sets/unoverload_type.ML` (diff)
Changeset 68437:f9b15e7c12bd by immler: restructured
The file was modified	`src/HOL/Types_To_Sets/unoverload_type.ML` (diff)
Changeset 68436:1b3edf5da4e4 by immler: result of unoverload is not in normal form
The file was modified	`src/HOL/Types_To_Sets/unoverload_type.ML` (diff)
Changeset 68435:2a2ef4552aaf by immler: tuned
The file was modified	`src/HOL/Types_To_Sets/unoverload_type.ML` (diff)
Changeset 68434:c6a38342376e by immler: allow for a list of vars
The file was modified	`src/HOL/Types_To_Sets/unoverload_type.ML` (diff)
Changeset 68433:f396f5490a8c by immler: parse var
The file was modified	`src/HOL/Types_To_Sets/unoverload_type.ML` (diff)