File ‹CTR_Algorithm.ML›

(* Title: CTR/CTR_Algorithm.ML
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins

Abstract interface for the definition of an algorithm for the synthesis
of transfer rules and relativized definitions.
*)

signature CTR_ALGORITHM =
sig

val apply : 
  Proof.context ->
  bool * thm list option ->
  thm list ->
  ((indexname * sort) * term) list ->
  thm -> 
  ctr_alg_out

end;