src/HOL/Library/Reflection.thy
changeset 46764 a65e18ceb1e3
parent 46510 696f3fec3f83
child 46765 07f9eda810b3
     1.1 --- a/src/HOL/Library/Reflection.thy	Fri Mar 02 15:17:54 2012 +0100
     1.2 +++ b/src/HOL/Library/Reflection.thy	Fri Mar 02 15:18:05 2012 +0100
     1.3 @@ -6,13 +6,13 @@
     1.4  
     1.5  theory Reflection
     1.6  imports Main
     1.7 -uses "reify_data.ML" ("reflection.ML")
     1.8 +uses
     1.9 +  "~~/src/HOL/Library/reify_data.ML"
    1.10 +  "~~/src/HOL/Library/reflection.ML"
    1.11  begin
    1.12  
    1.13  setup {* Reify_Data.setup *}
    1.14  
    1.15 -use "reflection.ML"
    1.16 -
    1.17  method_setup reify = {*
    1.18    Attrib.thms --
    1.19      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
    1.20 @@ -41,3 +41,4 @@
    1.21  *}
    1.22  
    1.23  end
    1.24 +