author | haftmann |
Sat, 24 Dec 2011 15:53:12 +0100 | |
changeset 45975 | 5e78c499a7ff |
parent 45231 | d85a2fdc586c |
permissions | -rw-r--r-- |
(* Title: HOL/Library/Executable_Set.thy Author: Stefan Berghofer, TU Muenchen Author: Florian Haftmann, TU Muenchen *) header {* A thin compatibility layer *} theory Executable_Set imports More_Set begin abbreviation Set :: "'a list \<Rightarrow> 'a set" where "Set \<equiv> set" abbreviation Coset :: "'a list \<Rightarrow> 'a set" where "Coset \<equiv> More_Set.coset" end