218 not (exists_subterm is_interesting_subterm t) orelse |
218 not (exists_subterm is_interesting_subterm t) orelse |
219 exists_type (exists_subtype (curry (op =) @{typ prop})) t |
219 exists_type (exists_subtype (curry (op =) @{typ prop})) t |
220 fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t |
220 fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t |
221 | is_boring_prop Ts (@{const "==>"} $ t $ u) = |
221 | is_boring_prop Ts (@{const "==>"} $ t $ u) = |
222 is_boring_prop Ts t andalso is_boring_prop Ts u |
222 is_boring_prop Ts t andalso is_boring_prop Ts u |
223 | is_boring_prop Ts (Const (@{const_name all}, _) $ (Abs (_, T, t)) $ u) = |
223 | is_boring_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) = |
224 is_boring_prop (T :: Ts) t andalso is_boring_prop (T :: Ts) u |
224 is_boring_prop (T :: Ts) t |
225 | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) = |
225 | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) = |
226 is_boring_prop Ts (t $ eta_expand Ts u 1) |
226 is_boring_prop Ts (t $ eta_expand Ts u 1) |
227 | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) = |
227 | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) = |
228 is_boring_bool t andalso is_boring_bool u |
228 is_boring_bool t andalso is_boring_bool u |
229 | is_boring_prop _ _ = true |
229 | is_boring_prop _ _ = true |