equal
deleted
inserted
replaced
5 section \<open>Ad Hoc Overloading\<close> |
5 section \<open>Ad Hoc Overloading\<close> |
6 |
6 |
7 theory Adhoc_Overloading_Examples |
7 theory Adhoc_Overloading_Examples |
8 imports |
8 imports |
9 Main |
9 Main |
10 "~~/src/HOL/Library/Infinite_Set" |
10 "HOL-Library.Infinite_Set" |
11 "~~/src/Tools/Adhoc_Overloading" |
11 "HOL-Library.Adhoc_Overloading" |
12 begin |
12 begin |
13 |
13 |
14 text \<open>Adhoc overloading allows to overload a constant depending on |
14 text \<open>Adhoc overloading allows to overload a constant depending on |
15 its type. Typically this involves to introduce an uninterpreted |
15 its type. Typically this involves to introduce an uninterpreted |
16 constant (used for input and output) and then add some variants (used |
16 constant (used for input and output) and then add some variants (used |