isabelle: src/HOL/Library/Adhoc_Overloading.thy@3dda49e08b9d (annotated)

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
48892 0b2407f406e8 prefer ML_file over old uses; wenzelm parents: 37818 diff changeset	13	ML_file "adhoc_overloading.ML"
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

author	wenzelm
	Fri, 04 Jan 2019 23:22:53 +0100
changeset 69593	3dda49e08b9d
parent 68061	81d90f830f99
child 69605	a96320074298
permissions	-rw-r--r--