equal
deleted
inserted
replaced
3 begin |
3 begin |
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 an equivariance rule *) |
9 (* we force it to be *) |
9 (* for the moment, we force it to be *) |
10 setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} |
10 setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} |
11 thm eqvts |
11 thm eqvts |
12 (*declare permute_pure[eqvt]*) |
12 (*declare permute_pure[eqvt]*) |
13 |
13 |
14 atom_decl var |
14 atom_decl var |