equal
deleted
inserted
replaced
1 theory Nominal |
1 theory Nominal |
2 imports Main "~~/src/HOL/Library/Infinite_Set" |
2 imports "~~/src/HOL/Library/Infinite_Set" "~~/src/HOL/Library/Old_Datatype" |
3 keywords |
3 keywords |
4 "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and |
4 "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and |
5 "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and |
5 "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and |
6 "avoids" |
6 "avoids" |
7 begin |
7 begin |