src/Tools/Adhoc_Overloading.thy
author wenzelm
Fri, 17 Apr 2015 22:15:35 +0200
changeset 60125 2944cc4f4f56
parent 58889 5b7a9633cfa8
child 62020 5d208fd2507d
permissions -rw-r--r--
tuned spelling;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     1
(* Author: Alexander Krauss, TU Muenchen
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     2
   Author: Christian Sternagel, University of Innsbruck
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     3
*)
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     4
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 52893
diff changeset
     5
section {* Adhoc overloading of constants based on their types *}
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     6
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
     7
theory Adhoc_Overloading
37818
dd65033fed78 load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents: 37789
diff changeset
     8
imports Pure
52622
e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents: 48892
diff changeset
     9
keywords "adhoc_overloading" :: thy_decl and  "no_adhoc_overloading" :: thy_decl
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    10
begin
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    11
48892
0b2407f406e8 prefer ML_file over old uses;
wenzelm
parents: 37818
diff changeset
    12
ML_file "adhoc_overloading.ML"
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    13
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents:
diff changeset
    14
end
37818
dd65033fed78 load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents: 37789
diff changeset
    15