| author | wenzelm | 
| Mon, 13 Sep 2021 11:58:11 +0200 | |
| changeset 74307 | de4b3abaf3ca | 
| 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: 
63432diff
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: 
63432diff
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: 
63432diff
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: 
63432diff
changeset | 9 | imports Main | 
| 
81d90f830f99
clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
 wenzelm parents: 
63432diff
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 |