File ‹unify_resolve.ML›
@{parse_entries (sig) PARSE_UNIFY_RESOLVE_ARGS
[normalisers, unifier, mode, chained, resolve_mode, rules]}
@{parse_entries (sig) PARSE_UNIFY_RESOLVE_CONTEXT_ARGS
[normalisers, unifier, mode, chained]}
@{parse_entries (sig) PARSE_UNIFY_RESOLVE_MODES [any, every]}
@{parse_entries (sig) PARSE_UNIFY_RESOLVE_CHAINED_MODES [insert, resolve, fact]}
@{parse_entries (sig) PARSE_UNIFY_RESOLVE_RESOLVE_MODES [r, rr, e, re, d, rd, f, rf]}
signature UNIFY_RESOLVE_ARGS =
sig
include HAS_LOGGER
structure PA : PARSE_UNIFY_RESOLVE_ARGS
structure PCA : PARSE_UNIFY_RESOLVE_CONTEXT_ARGS
val PCA_entries_from_PA_entries : ('a, 'b, 'c, 'd, 'e, 'f) PA.entries -> ('a, 'b, 'c, 'd) PCA.entries
val PA_entries_from_PCA_entries : ('a, 'b, 'c, 'd) PCA.entries -> 'e -> 'f ->
('a, 'b, 'c, 'd, 'e, 'f) PA.entries
structure PM : PARSE_UNIFY_RESOLVE_MODES
type mode = PM.key
val parse_mode : mode parser
structure PCM : PARSE_UNIFY_RESOLVE_CHAINED_MODES
type chained_mode = PCM.key
val parse_chained_mode : chained_mode parser
structure PRM : PARSE_UNIFY_RESOLVE_RESOLVE_MODES
type resolve_mode = PRM.key
val parse_resolve_mode : resolve_mode parser
type args = (Unification_Base.normalisers, Unification_Base.unifier, mode, chained_mode,
resolve_mode, thm list) PA.entries
type context_args = (Unification_Base.normalisers, Unification_Base.unifier, mode,
chained_mode) PCA.entries
val unify_resolve_tac : args -> thm list -> Proof.context -> int -> tactic
val unify_resolve_context_args_tac : context_args -> resolve_mode -> thm list -> thm list ->
Proof.context -> int -> tactic
val arg_parsers : (ML_Code_Util.code parser, ML_Code_Util.code parser, mode parser,
chained_mode parser, resolve_mode parser, thm list context_parser) PA.entries
end
structure Unify_Resolve_Args : UNIFY_RESOLVE_ARGS =
struct
structure URB = Unify_Resolve_Base
val logger = Logger.setup_new_logger URB.logger "Unify_Resolve_Args"