doc-src/IsarImplementation/Thy/prelim.thy
changeset 20547 796ae7fa1049
parent 20530 448594cbd82b
child 21852 7f2853bd54bf
equal deleted inserted replaced
20546:8923deb735ad 20547:796ae7fa1049
   150   \begin{mldecls}
   150   \begin{mldecls}
   151   @{index_ML_type theory} \\
   151   @{index_ML_type theory} \\
   152   @{index_ML Theory.subthy: "theory * theory -> bool"} \\
   152   @{index_ML Theory.subthy: "theory * theory -> bool"} \\
   153   @{index_ML Theory.merge: "theory * theory -> theory"} \\
   153   @{index_ML Theory.merge: "theory * theory -> theory"} \\
   154   @{index_ML Theory.checkpoint: "theory -> theory"} \\
   154   @{index_ML Theory.checkpoint: "theory -> theory"} \\
   155   @{index_ML Theory.copy: "theory -> theory"} \\[1ex]
   155   @{index_ML Theory.copy: "theory -> theory"} \\
       
   156   \end{mldecls}
       
   157   \begin{mldecls}
   156   @{index_ML_type theory_ref} \\
   158   @{index_ML_type theory_ref} \\
   157   @{index_ML Theory.self_ref: "theory -> theory_ref"} \\
   159   @{index_ML Theory.self_ref: "theory -> theory_ref"} \\
   158   @{index_ML Theory.deref: "theory_ref -> theory"} \\
   160   @{index_ML Theory.deref: "theory_ref -> theory"} \\
   159   \end{mldecls}
   161   \end{mldecls}
   160 
   162 
   478   @{index_ML_type "Symbol.symbol"} \\
   480   @{index_ML_type "Symbol.symbol"} \\
   479   @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
   481   @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
   480   @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
   482   @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
   481   @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
   483   @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
   482   @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
   484   @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
   483   @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\[1ex]
   485   @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
       
   486   \end{mldecls}
       
   487   \begin{mldecls}
   484   @{index_ML_type "Symbol.sym"} \\
   488   @{index_ML_type "Symbol.sym"} \\
   485   @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
   489   @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
   486   \end{mldecls}
   490   \end{mldecls}
   487 
   491 
   488   \begin{description}
   492   \begin{description}
   550 *}
   554 *}
   551 
   555 
   552 text %mlref {*
   556 text %mlref {*
   553   \begin{mldecls}
   557   \begin{mldecls}
   554   @{index_ML Name.internal: "string -> string"} \\
   558   @{index_ML Name.internal: "string -> string"} \\
   555   @{index_ML Name.skolem: "string -> string"} \\[1ex]
   559   @{index_ML Name.skolem: "string -> string"} \\
       
   560   \end{mldecls}
       
   561   \begin{mldecls}
   556   @{index_ML_type Name.context} \\
   562   @{index_ML_type Name.context} \\
   557   @{index_ML Name.context: Name.context} \\
   563   @{index_ML Name.context: Name.context} \\
   558   @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
   564   @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
   559   @{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\
   565   @{index_ML Name.invents: "Name.context -> string -> int -> string list"} \\
   560   @{index_ML Name.variants: "string list -> Name.context -> string list * Name.context"} \\
   566   @{index_ML Name.variants: "string list -> Name.context -> string list * Name.context"} \\
   695   \begin{mldecls}
   701   \begin{mldecls}
   696   @{index_ML NameSpace.base: "string -> string"} \\
   702   @{index_ML NameSpace.base: "string -> string"} \\
   697   @{index_ML NameSpace.qualifier: "string -> string"} \\
   703   @{index_ML NameSpace.qualifier: "string -> string"} \\
   698   @{index_ML NameSpace.append: "string -> string -> string"} \\
   704   @{index_ML NameSpace.append: "string -> string -> string"} \\
   699   @{index_ML NameSpace.pack: "string list -> string"} \\
   705   @{index_ML NameSpace.pack: "string list -> string"} \\
   700   @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex]
   706   @{index_ML NameSpace.unpack: "string -> string list"} \\
       
   707   \end{mldecls}
       
   708   \begin{mldecls}
   701   @{index_ML_type NameSpace.naming} \\
   709   @{index_ML_type NameSpace.naming} \\
   702   @{index_ML NameSpace.default_naming: NameSpace.naming} \\
   710   @{index_ML NameSpace.default_naming: NameSpace.naming} \\
   703   @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
   711   @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
   704   @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\[1ex]
   712   @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\
       
   713   \end{mldecls}
       
   714   \begin{mldecls}
   705   @{index_ML_type NameSpace.T} \\
   715   @{index_ML_type NameSpace.T} \\
   706   @{index_ML NameSpace.empty: NameSpace.T} \\
   716   @{index_ML NameSpace.empty: NameSpace.T} \\
   707   @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
   717   @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
   708   @{index_ML NameSpace.declare: "NameSpace.naming -> string -> NameSpace.T -> NameSpace.T"} \\
   718   @{index_ML NameSpace.declare: "NameSpace.naming -> string -> NameSpace.T -> NameSpace.T"} \\
   709   @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
   719   @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\