30 fun minus_permute_elim p thm = |
30 fun minus_permute_elim p thm = |
31 thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI}) |
31 thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI}) |
32 |
32 |
33 (* fixme: move to nominal_library *) |
33 (* fixme: move to nominal_library *) |
34 fun real_head_of (@{term Trueprop} $ t) = real_head_of t |
34 fun real_head_of (@{term Trueprop} $ t) = real_head_of t |
35 | real_head_of (Const ("==>", _) $ _ $ t) = real_head_of t |
35 | real_head_of (Const (@{const_name Pure.imp}, _) $ _ $ t) = real_head_of t |
36 | real_head_of (Const (@{const_name all}, _) $ Abs (_, _, t)) = real_head_of t |
36 | real_head_of (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = real_head_of t |
37 | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t |
37 | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t |
38 | real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t |
38 | real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t |
39 | real_head_of t = head_of t |
39 | real_head_of t = head_of t |
40 |
40 |
41 |
41 |