equal
deleted
inserted
replaced
1 header \<open>Dummy theory to anticipate AFP/Nominal2 keywords\<close> (* Proof General legacy *) |
|
2 |
|
3 theory Nominal2_Dummy |
|
4 imports Main |
|
5 keywords |
|
6 "nominal_datatype" :: thy_decl and |
|
7 "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal and |
|
8 "atom_decl" "equivariance" :: thy_decl and |
|
9 "avoids" "binds" |
|
10 begin |
|
11 |
|
12 ML \<open> |
|
13 Outer_Syntax.command @{command_spec "nominal_datatype"} "dummy" Scan.fail; |
|
14 Outer_Syntax.command @{command_spec "nominal_function"} "dummy" Scan.fail; |
|
15 Outer_Syntax.command @{command_spec "nominal_inductive"} "dummy" Scan.fail; |
|
16 Outer_Syntax.command @{command_spec "nominal_termination"} "dummy" Scan.fail; |
|
17 Outer_Syntax.command @{command_spec "atom_decl"} "dummy" Scan.fail; |
|
18 Outer_Syntax.command @{command_spec "equivariance"} "dummy" Scan.fail; |
|
19 \<close> |
|
20 |
|
21 end |
|
22 |
|