12 months ago immler [Wed, 13 Jun 2018 10:45:23 +0200] rev 68437
restructured
src/HOL/Types_To_Sets/unoverload_type.ML

12 months ago immler [Wed, 13 Jun 2018 09:38:07 +0200] rev 68436
result of unoverload is not in normal form
src/HOL/Types_To_Sets/unoverload_type.ML

12 months ago immler [Wed, 13 Jun 2018 09:26:04 +0200] rev 68435
tuned
src/HOL/Types_To_Sets/unoverload_type.ML

12 months ago immler [Wed, 13 Jun 2018 09:22:58 +0200] rev 68434
allow for a list of vars
src/HOL/Types_To_Sets/unoverload_type.ML

12 months ago immler [Wed, 13 Jun 2018 09:11:35 +0200] rev 68433
parse var
src/HOL/Types_To_Sets/unoverload_type.ML

12 months ago nipkow [Tue, 12 Jun 2018 19:37:47 +0200] rev 68432
merged

12 months ago nipkow [Tue, 12 Jun 2018 17:18:40 +0200] rev 68431
more abstract naming
src/HOL/Data_Structures/AA_Map.thy src/HOL/Data_Structures/AA_Set.thy src/HOL/Data_Structures/AVL_Map.thy src/HOL/Data_Structures/AVL_Set.thy src/HOL/Data_Structures/Brother12_Map.thy src/HOL/Data_Structures/Brother12_Set.thy src/HOL/Data_Structures/Map_Specs.thy src/HOL/Data_Structures/RBT_Map.thy src/HOL/Data_Structures/RBT_Set.thy src/HOL/Data_Structures/Tree234_Map.thy src/HOL/Data_Structures/Tree234_Set.thy src/HOL/Data_Structures/Tree23_Map.thy src/HOL/Data_Structures/Tree23_Set.thy src/HOL/Data_Structures/Tree_Map.thy src/HOL/Data_Structures/Tree_Set.thy

12 months ago immler [Tue, 12 Jun 2018 19:32:42 +0200] rev 68430
tuned
src/HOL/Types_To_Sets/unoverload_type.ML

12 months ago immler [Tue, 12 Jun 2018 19:30:55 +0200] rev 68429
workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
src/HOL/Types_To_Sets/unoverload_type.ML

12 months ago immler [Tue, 12 Jun 2018 16:21:52 +0200] rev 68428
a derived rule combining unoverload and internalize_sort
src/HOL/Types_To_Sets/Examples/T2_Spaces.thy src/HOL/Types_To_Sets/Types_To_Sets.thy src/HOL/Types_To_Sets/unoverload_type.ML