src/Tools/Adhoc_Overloading.thy
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 52893 aa2afbafd983
child 58889 5b7a9633cfa8
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
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
52893
aa2afbafd983 use uniform spelling of "adhoc"
Christian Sternagel
parents: 52622
diff changeset
     5
header {* 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