equal
deleted
inserted
replaced
28 lemmas [symmetric, code inline] = subset_def |
28 lemmas [symmetric, code inline] = subset_def |
29 |
29 |
30 lemma [code target: Set]: |
30 lemma [code target: Set]: |
31 "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
31 "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
32 by blast |
32 by blast |
33 |
|
34 lemma [code func]: |
|
35 "Code_Generator.eq A B \<longleftrightarrow> subset A B \<and> subset B A" |
|
36 unfolding eq_def subset_def by blast |
|
37 |
33 |
38 lemma [code func]: |
34 lemma [code func]: |
39 "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
35 "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
40 unfolding subset_def Set.subset_def .. |
36 unfolding subset_def Set.subset_def .. |
41 |
37 |