src/HOL/Library/Adhoc_Overloading.thy
author wenzelm
Tue, 01 May 2018 20:40:27 +0200
changeset 68061 81d90f830f99
parent 63432 src/Tools/Adhoc_Overloading.thy@ba7901e94e7b
child 69605 a96320074298
permissions -rw-r--r--
clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations); tuned headers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     4
*)
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     5
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
     6
section \<open>Adhoc overloading of constants based on their types\<close>
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     7
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     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
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    11
begin
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    12
48892
0b2407f406e8 prefer ML_file over old uses;
wenzelm
parents: 37818
diff changeset
    13
ML_file "adhoc_overloading.ML"
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    14
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    15
end