author | haftmann |
Wed, 13 Dec 2006 20:38:17 +0100 | |
changeset 21833 | b6e4c5578c8e |
parent 21832 | 5a6f8514d0e9 |
child 21834 | 770ce948a59b |
src/HOL/Set.thy | file | annotate | diff | comparison | revisions |
--- 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 ();