author | Lars Hupel <lars.hupel@mytum.de> |
Mon, 18 Jun 2018 10:50:24 +0200 | |
changeset 68462 | 8d1bf38c6fe6 |
parent 68061 | 81d90f830f99 |
child 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 |
||
48892 | 13 |
ML_file "adhoc_overloading.ML" |
37789 | 14 |
|
15 |
end |