Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/quotient_tacs.ML
changeset 870 2a19e0a37131
parent 866 f537d570fff8
child 871 4163fe3dbf8c
equal deleted inserted replaced
869:ce5f78f0eac5 870:2a19e0a37131 
    55   REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
 
    55   REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
 
    56 
    56 
    57 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 
    57 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 
    58 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
    58 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
    59 
    59 
    60 fun quotient_tac ctxt = SOLVED'
 
    60 fun quotient_tac ctxt =
 
    61   (REPEAT_ALL_NEW (FIRST'
 
    61   (REPEAT_ALL_NEW (FIRST'
 
    62     [rtac @{thm identity_quotient},
 
    62     [rtac @{thm identity_quotient},
 
    63      resolve_tac (quotient_rules_get ctxt)]))
 
    63      resolve_tac (quotient_rules_get ctxt)]))
 
    64 
    64 
    65 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
 
    65 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
nominal2