author | haftmann |
Sat, 24 Dec 2011 15:53:12 +0100 | |
changeset 45975 | 5e78c499a7ff |
parent 45231 | d85a2fdc586c |
permissions | -rw-r--r-- |
34020 | 1 |
(* Title: HOL/Library/Executable_Set.thy |
2 |
Author: Stefan Berghofer, TU Muenchen |
|
33947 | 3 |
Author: Florian Haftmann, TU Muenchen |
4 |
*) |
|
5 |
||
45975 | 6 |
header {* A thin compatibility layer *} |
33947 | 7 |
|
34020 | 8 |
theory Executable_Set |
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
9 |
imports More_Set |
33947 | 10 |
begin |
11 |
||
45975 | 12 |
abbreviation Set :: "'a list \<Rightarrow> 'a set" where |
13 |
"Set \<equiv> set" |
|
33947 | 14 |
|
45975 | 15 |
abbreviation Coset :: "'a list \<Rightarrow> 'a set" where |
16 |
"Coset \<equiv> More_Set.coset" |
|
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
17 |
|
33947 | 18 |
end |