blob: 7cd7a08c6e1d567408f54e2e65203ec56a9b2adb (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
signature external_OpaqueTheory =
sig
type thm = Thm.thm
val external_Opaque_grammars : type_grammar.grammar * term_grammar.grammar
(*
[external_Types] Parent theory of "external_Opaque"
*)
end
|