# HG changeset patch
# User blanchet
# Date 1450551771 -3600
# Node ID edceda92a43520b37e0df46ba88ee14ecc3dd6c6
# Parent  3f494c048142cb5bbca27d4609b7f72fa08a3bed
removed subsumed dependency

diff -r 3f494c048142 -r edceda92a435 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat Dec 19 20:02:51 2015 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Sat Dec 19 20:02:51 2015 +0100
@@ -6,7 +6,7 @@
 section \<open>Hilbert's Epsilon-Operator and the Axiom of Choice\<close>
 
 theory Hilbert_Choice
-imports Nat Wellfounded
+imports Wellfounded
 keywords "specification" :: thy_goal
 begin