| changeset 21046 | fe1db2f991a7 |
| parent 21008 | 330a8a6dd53c |
| child 21063 | 3c5074f028c8 |
--- a/src/HOL/Library/ExecutableSet.thy Mon Oct 16 14:07:21 2006 +0200 +++ b/src/HOL/Library/ExecutableSet.thy Mon Oct 16 14:07:31 2006 +0200 @@ -18,7 +18,7 @@ by blast lemma [code func]: - "OperationalEquality.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)" + "Code_Generator.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)" unfolding eq_def by blast declare bex_triv_one_point1 [symmetric, standard, code]