equal
deleted
inserted
replaced
1 theory FSet3 |
1 theory FSet3 |
2 imports "../QuotMain" "../QuotList" List |
2 imports "../QuotMain" "../QuotList" List |
3 begin |
3 begin |
|
4 |
|
5 ML {* |
|
6 structure QuotientRules = Named_Thms |
|
7 (val name = "quot_thm" |
|
8 val description = "Quotient theorems.") |
|
9 *} |
|
10 |
|
11 ML {* |
|
12 open QuotientRules |
|
13 *} |
4 |
14 |
5 fun |
15 fun |
6 list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50) |
16 list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50) |
7 where |
17 where |
8 "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)" |
18 "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)" |