summaryrefslogtreecommitdiff
path: root/tests/hol4/betree/betreeMain_OpaqueTheory.sig
blob: da7559a00f741ffe384c9af276e93285e3fa7b53 (plain)
1
2
3
4
5
6
7
8
9
10
11
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