| author | wenzelm | 
| Mon, 24 Aug 2020 21:47:21 +0200 | |
| changeset 72202 | 0840240dfb24 | 
| parent 69605 | a96320074298 | 
| permissions | -rw-r--r-- | 
| 
68061
 
81d90f830f99
clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
 
wenzelm 
parents: 
63432 
diff
changeset
 | 
1  | 
(* Title: HOL/Library/Adhoc_Overloading.thy  | 
| 
 
81d90f830f99
clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
 
wenzelm 
parents: 
63432 
diff
changeset
 | 
2  | 
Author: Alexander Krauss, TU Muenchen  | 
| 
 
81d90f830f99
clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
 
wenzelm 
parents: 
63432 
diff
changeset
 | 
3  | 
Author: Christian Sternagel, University of Innsbruck  | 
| 37789 | 4  | 
*)  | 
5  | 
||
| 62020 | 6  | 
section \<open>Adhoc overloading of constants based on their types\<close>  | 
| 37789 | 7  | 
|
8  | 
theory Adhoc_Overloading  | 
|
| 
68061
 
81d90f830f99
clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
 
wenzelm 
parents: 
63432 
diff
changeset
 | 
9  | 
imports Main  | 
| 
 
81d90f830f99
clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
 
wenzelm 
parents: 
63432 
diff
changeset
 | 
10  | 
keywords "adhoc_overloading" "no_adhoc_overloading" :: thy_decl  | 
| 37789 | 11  | 
begin  | 
12  | 
||
| 69605 | 13  | 
ML_file \<open>adhoc_overloading.ML\<close>  | 
| 37789 | 14  | 
|
15  | 
end  |