changeset 21833 | b6e4c5578c8e |
parent 21819 | 8eb82ffcdd15 |
child 22139 | 539a63b98f76 |
--- a/src/HOL/Set.thy Wed Dec 13 20:38:16 2006 +0100 +++ b/src/HOL/Set.thy Wed Dec 13 20:38:17 2006 +0100 @@ -226,7 +226,6 @@ "\<exists>A\<subseteq>B. P" => "EX A. A \<subseteq> B & P" "\<exists>!A\<subseteq>B. P" => "EX! A. A \<subseteq> B & P" -(* FIXME re-use version in Orderings.thy *) print_translation {* let val thy = the_context ();