--- a/src/HOL/Library/Reflection.thy Fri Mar 02 15:17:54 2012 +0100
+++ b/src/HOL/Library/Reflection.thy Fri Mar 02 15:18:05 2012 +0100
@@ -6,13 +6,13 @@
theory Reflection
imports Main
-uses "reify_data.ML" ("reflection.ML")
+uses
+ "~~/src/HOL/Library/reify_data.ML"
+ "~~/src/HOL/Library/reflection.ML"
begin
setup {* Reify_Data.setup *}
-use "reflection.ML"
-
method_setup reify = {*
Attrib.thms --
Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
@@ -41,3 +41,4 @@
*}
end
+