src/Tools/Adhoc_Overloading.thy
author wenzelm
Fri, 07 Mar 2014 16:00:45 +0100
changeset 55979 06cb126f30ba
parent 52893 aa2afbafd983
child 58889 5b7a9633cfa8
permissions -rw-r--r--
tuned message: reveal ambiguity where Syntax_Phases.decode_term fails and thus reduces proper_results beforehand, e.g. term "f(x := y)" in ~~/src/HOL/Hoare/Hoare_Logic.thy;
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