src/Tools/Adhoc_Overloading.thy
author wenzelm
Thu, 07 Apr 2016 20:51:52 +0200
changeset 62908 d7009a515733
parent 62020 5d208fd2507d
child 63432 ba7901e94e7b
permissions -rw-r--r--
clarified mode of ROOT.ML files;
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
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 58889
diff changeset
     5
section \<open>Adhoc overloading of constants based on their types\<close>
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