src/HOL/ex/Nominal2_Dummy.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 57064 8a1be5efe628
permissions -rw-r--r--
specialized specification: avoid trivial instances
wenzelm@57064
     1
header \<open>Dummy theory to anticipate AFP/Nominal2 keywords\<close>  (* Proof General legacy *)
wenzelm@57064
     2
wenzelm@57064
     3
theory Nominal2_Dummy
wenzelm@57064
     4
imports Main
wenzelm@57064
     5
keywords
wenzelm@57064
     6
  "nominal_datatype" :: thy_decl and
wenzelm@57064
     7
  "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and
wenzelm@57064
     8
  "atom_decl" "equivariance" :: thy_decl and
wenzelm@57064
     9
  "avoids" "binds"
wenzelm@57064
    10
begin
wenzelm@57064
    11
wenzelm@57064
    12
ML \<open>
wenzelm@57064
    13
Outer_Syntax.command @{command_spec "nominal_datatype"} "dummy" Scan.fail;
wenzelm@57064
    14
Outer_Syntax.command @{command_spec "nominal_function"} "dummy" Scan.fail;
wenzelm@57064
    15
Outer_Syntax.command @{command_spec "nominal_inductive"} "dummy" Scan.fail;
wenzelm@57064
    16
Outer_Syntax.command @{command_spec "nominal_termination"} "dummy" Scan.fail;
wenzelm@57064
    17
Outer_Syntax.command @{command_spec "atom_decl"} "dummy" Scan.fail;
wenzelm@57064
    18
Outer_Syntax.command @{command_spec "equivariance"} "dummy" Scan.fail;
wenzelm@57064
    19
\<close>
wenzelm@57064
    20
wenzelm@57064
    21
end
wenzelm@57064
    22