equal
deleted
inserted
replaced
18 |
18 |
19 structure Nominal_Inductive : NOMINAL_INDUCTIVE = |
19 structure Nominal_Inductive : NOMINAL_INDUCTIVE = |
20 struct |
20 struct |
21 |
21 |
22 |
22 |
23 fun mk_cplus p q = Thm.capply (Thm.capply @{cterm "plus :: perm => perm => perm"} p) q |
23 fun mk_cplus p q = Thm.apply (Thm.apply @{cterm "plus :: perm => perm => perm"} p) q |
24 |
24 |
25 fun mk_cminus p = Thm.capply @{cterm "uminus :: perm => perm"} p |
25 fun mk_cminus p = Thm.apply @{cterm "uminus :: perm => perm"} p |
26 |
26 |
27 fun minus_permute_intro_tac p = |
27 fun minus_permute_intro_tac p = |
28 rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}) |
28 rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}) |
29 |
29 |
30 fun minus_permute_elim p thm = |
30 fun minus_permute_elim p thm = |