src/HOL/Library/Adhoc_Overloading.thy
author wenzelm
Tue, 22 Oct 2019 20:55:13 +0200
changeset 70923 98d9b78b7f47
parent 69605 a96320074298
permissions -rw-r--r--
clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;
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