Theory ETTS_Tools

(* Title: ETTS/ETTS_Tools/ETTS_Tools.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins

A collection of basic Isabelle/ML functions for the ETTS.
*)

section‹Import›
theory ETTS_Tools
  imports "Conditional_Transfer_Rule.CTR_Tools"
begin



subsection‹Auxiliary›

lemma tr_to_tr_rel: "A b c ⟹ (Transfer.Rel A) b c"
  unfolding Transfer.Rel_def .



subsection‹Standard library extension›

ML_file "More_Library.ML"
ML_file "More_Logic.ML"
ML_file "More_Tactical.ML"
ML_file "More_Simplifier.ML"
ML_file "More_HOLogic.ML"
ML_file "More_Transfer.ML"



subsection‹Specialized functionality›

ML_file "ETTS_Writer.ML"

end