equal
deleted
inserted
replaced
591 |> scope <> Global ? cons local_feature |
591 |> scope <> Global ? cons local_feature |
592 |> exists (not o is_lambda_free) ts ? cons lams_feature |
592 |> exists (not o is_lambda_free) ts ? cons lams_feature |
593 |> exists (exists_Const is_exists) ts ? cons skos_feature |
593 |> exists (exists_Const is_exists) ts ? cons skos_feature |
594 end |
594 end |
595 |
595 |
596 (* Too many dependencies is a sign that a crazy decision procedure is at work. |
596 (* Too many dependencies is a sign that a decision procedure is at work. There |
597 There isn't much to learn from such proofs. *) |
597 isn't much to learn from such proofs. *) |
598 val max_dependencies = 10 |
598 val max_dependencies = 20 |
599 val atp_dependency_default_max_facts = 50 |
599 val atp_dependency_default_max_facts = 50 |
600 |
600 |
601 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) |
601 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) |
602 val typedef_deps = [@{thm CollectI} |> nickname_of] |
602 val typedef_deps = [@{thm CollectI} |> nickname_of] |
603 |
603 |