src/HOL/Lifting.thy
changeset 47698 18202d3d5832
parent 47652 1b722b100301
child 47777 f29e7dcd7c40
--- a/src/HOL/Lifting.thy	Mon Apr 23 16:30:43 2012 +0200
+++ b/src/HOL/Lifting.thy	Mon Apr 23 17:18:18 2012 +0200
@@ -12,6 +12,7 @@
   "lift_definition" :: thy_goal and
   "setup_lifting" :: thy_decl
 uses
+  ("Tools/Lifting/lifting_util.ML")
   ("Tools/Lifting/lifting_info.ML")
   ("Tools/Lifting/lifting_term.ML")
   ("Tools/Lifting/lifting_def.ML")
@@ -354,7 +355,7 @@
 
 subsection {* ML setup *}
 
-text {* Auxiliary data for the lifting package *}
+use "Tools/Lifting/lifting_util.ML"
 
 use "Tools/Lifting/lifting_info.ML"
 setup Lifting_Info.setup