1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Nominal2_Dummy.thy	Thu May 22 15:49:36 2014 +0200
     1.3 @@ -0,0 +1,22 @@
     1.4 +header \<open>Dummy theory to anticipate AFP/Nominal2 keywords\<close>  (* Proof General legacy *)
     1.5 +
     1.6 +theory Nominal2_Dummy
     1.7 +imports Main
     1.8 +keywords
     1.9 +  "nominal_datatype" :: thy_decl and
    1.10 +  "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and
    1.11 +  "atom_decl" "equivariance" :: thy_decl and
    1.12 +  "avoids" "binds"
    1.13 +begin
    1.14 +
    1.15 +ML \<open>
    1.16 +Outer_Syntax.command @{command_spec "nominal_datatype"} "dummy" Scan.fail;
    1.17 +Outer_Syntax.command @{command_spec "nominal_function"} "dummy" Scan.fail;
    1.18 +Outer_Syntax.command @{command_spec "nominal_inductive"} "dummy" Scan.fail;
    1.19 +Outer_Syntax.command @{command_spec "nominal_termination"} "dummy" Scan.fail;
    1.20 +Outer_Syntax.command @{command_spec "atom_decl"} "dummy" Scan.fail;
    1.21 +Outer_Syntax.command @{command_spec "equivariance"} "dummy" Scan.fail;
    1.22 +\<close>
    1.23 +
    1.24 +end
    1.25 +