src/HOL/Library/Adhoc_Overloading.thy
author wenzelm
Tue, 05 Nov 2019 14:16:16 +0100
changeset 71046 b8aeeedf7e68
parent 69605 a96320074298
permissions -rw-r--r--
support for Linux user management;
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
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 68061
diff changeset
    13
ML_file \<open>adhoc_overloading.ML\<close>
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