equal
deleted
inserted
replaced
16 lemma [code target: Set]: |
16 lemma [code target: Set]: |
17 "(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)" |
17 "(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)" |
18 by blast |
18 by blast |
19 |
19 |
20 lemma [code func]: |
20 lemma [code func]: |
21 "OperationalEquality.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)" |
21 "Code_Generator.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)" |
22 unfolding eq_def by blast |
22 unfolding eq_def by blast |
23 |
23 |
24 declare bex_triv_one_point1 [symmetric, standard, code] |
24 declare bex_triv_one_point1 [symmetric, standard, code] |
25 |
25 |
26 |
26 |