Theory IsaFoR_Nonground_Clause

theory IsaFoR_Nonground_Clause
  imports 
    IsaFoR_Nonground_Term
    Nonground_Clause
begin

interpretation nonground_clause where
  comp_subst = "(∘s)" and id_subst = Var and subst_update = fun_upd and
  apply_subst = apply_subst and term_subst = "(⋅)" and term_vars = vars_term and
  term_to_ground = term.to_ground and  term_from_ground = term.from_ground and
  term_is_ground = term.is_ground
  by unfold_locales

end