Proof Example
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
This commit is contained in:
parent
4c4194d468
commit
869644e3b5
|
@ -564,10 +564,10 @@ Type_Infer_Context.infer_types: Proof.context -> term list -> term list
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
subsection*[t233::technical]\<open> theories and the signature interface\<close>
|
subsection*[t233::technical]\<open> Theories and the Signature API\<close>
|
||||||
ML\<open>
|
ML\<open>
|
||||||
Sign.tsig_of: theory -> Type.tsig;
|
Sign.tsig_of : theory -> Type.tsig;
|
||||||
Sign.syn_of : theory -> Syntax.syntax;
|
Sign.syn_of : theory -> Syntax.syntax;
|
||||||
Sign.of_sort : theory -> typ * sort -> bool ;
|
Sign.of_sort : theory -> typ * sort -> bool ;
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue