src/HOL/Decision_Procs/Ferrack.thy
changeset 44013 5cfc1c36ae97
parent 42361 23f352990944
child 44779 98d597c4193d
--- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
 
 theory Ferrack
 imports Complex_Main Dense_Linear_Order DP_Library
-  "~~/src/HOL/Library/Efficient_Nat"
+  "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
 uses ("ferrack_tac.ML")
 begin