src/HOL/Hilbert_Choice.thy
changeset 26748 4d51ddd6aa5c
parent 26562 9d25ef112cf6
child 27760 3aa86edac080
--- a/src/HOL/Hilbert_Choice.thy	Thu Apr 24 16:53:04 2008 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Fri Apr 25 15:30:33 2008 +0200
@@ -7,7 +7,7 @@
 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
 
 theory Hilbert_Choice
-imports Nat Wellfounded_Recursion
+imports Nat Wellfounded
 uses ("Tools/meson.ML") ("Tools/specification_package.ML")
 begin