Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Nominal2_Dummy.thy
author wenzelm
Thu, 22 May 2014 15:49:36 +0200
changeset 57064 8a1be5efe628
permissions -rw-r--r--
include Nominal2 keywords -- Proof General legacy;

header \<open>Dummy theory to anticipate AFP/Nominal2 keywords\<close>  (* Proof General legacy *)

theory Nominal2_Dummy
imports Main
keywords
  "nominal_datatype" :: thy_decl and
  "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and
  "atom_decl" "equivariance" :: thy_decl and
  "avoids" "binds"
begin

ML \<open>
Outer_Syntax.command @{command_spec "nominal_datatype"} "dummy" Scan.fail;
Outer_Syntax.command @{command_spec "nominal_function"} "dummy" Scan.fail;
Outer_Syntax.command @{command_spec "nominal_inductive"} "dummy" Scan.fail;
Outer_Syntax.command @{command_spec "nominal_termination"} "dummy" Scan.fail;
Outer_Syntax.command @{command_spec "atom_decl"} "dummy" Scan.fail;
Outer_Syntax.command @{command_spec "equivariance"} "dummy" Scan.fail;
\<close>

end
isabelle