signature betreeMain_OpaqueTheory = sig type thm = Thm.thm val betreeMain_Opaque_grammars : type_grammar.grammar * term_grammar.grammar (* [betreeMain_Types] Parent theory of "betreeMain_Opaque" *) end