equal
deleted
inserted
replaced
4 |
4 |
5 (* core haskell *) |
5 (* core haskell *) |
6 |
6 |
7 ML {* val _ = recursive := false *} |
7 ML {* val _ = recursive := false *} |
8 (* this should not be a raw equivariant rule *) |
8 (* this should not be a raw equivariant rule *) |
9 declare permute_pure[eqvt] |
9 (* we force it to be *) |
10 |
10 setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} |
|
11 thm eqvts |
|
12 (*declare permute_pure[eqvt]*) |
11 |
13 |
12 atom_decl var |
14 atom_decl var |
13 atom_decl cvar |
15 atom_decl cvar |
14 atom_decl tvar |
16 atom_decl tvar |
15 |
17 |