/seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
H A D | quotient_optionScript.sml | 38 (* Type Operator Constructor Abstraction Equivalence *)
|
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | Diff.sml | 8 val (Type, Term) = parse_from_grammars limTheory.lim_grammars value
|
/seL4-l4v-10.1.1/HOL4/src/refute/ |
H A D | Canon.sml | 46 and aty = Type.alpha 62 Ty=(type_of v --> Type.bool) --> type_of v} 634 and aty = Type.alpha 694 val (atys,_) = splitlist Type.dom_rng (type_of v)
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttExec.sml | 42 Type of values
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/acl2/ |
H A D | m1_progLib.sml | 76 val ty = Parse.Type [QUOTE (":" ^ ff (dest_tuple input))]
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/MARS/ |
H A D | MARS_DataScript.sml | 13 (* Type Definitions *)
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | ExportTree.sml | 28 | PTtype of types (* Type of an expression *)
|
H A D | COPIER.sml | 63 (* Type constructor cache. This maps typeIDs in the copied signature to 145 buildTypeCache(sourceTab, strName, mapTypeId, false, (* Type abbreviations. *)datatypeCache, datatypeCache)
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | TypeBase.sml | 109 ("Type information for: " ^ 222 case Type.op_arity{Tyop=nm,Thy=thy} of
|
H A D | selftest.sml | 25 val x = mk_var("x", Type.alpha) 26 val xfun = mk_var("x", Type.alpha --> Type.alpha) 27 val y = mk_var("y", Type.alpha) 281 if Type.compare(randty, alpha --> bool) <> EQUAL then die "" 309 val ty = Parse.Type [QUOTE s] 505 val res = thm_to_string (ASSUME (mk_var("p", Type.bool)))
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | SmtLib_Theories.sml | 137 ("Array", K_zero_two Type.-->) 215 ("Bool", K_zero_zero Type.bool)
|
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | holindexData.sml | 286 | update_data_store (allow_new,error_fun) (sds_thm,sds_term,sds_type) "Type" key upf = 288 (allow_new, unknown_def ("Type", error_fun)) sds_type key upf)
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | listSimps.sml | 14 val (Type,Term) = parse_from_grammars listTheory.list_grammars value 15 fun == q x = Type q
|
H A D | ListConv1.sml | 50 val (Type,Term) = parse_from_grammars rich_listTheory.rich_list_grammars value 51 fun == q x = Type q 56 val alpha_ty = Type.alpha 57 val bool_ty = Type.bool; 495 [Type.alpha |-> lty, Type.beta |-> ety]) ithm 615 (Thm.INST_TYPE [Type.alpha |-> ty] listTheory.REV_DEF)
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Parse.sig | 4 type hol_type = Type.hol_type 26 val Type : hol_type frag list -> hol_type value
|
H A D | parse_type.sml | 300 ("Type parsing failure with remaining input: "^ 307 ("Type-atom parsing failure with remaining input: "^
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | boolSimps.sml | 229 open Type Rsyntax 336 open Type
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | stats.py | 3 from syntax import Expr, Type namespace
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/prog/ |
H A D | x64_progLib.sml | 10 val (Type, Term) = parse_from_grammars x64_progTheory.x64_prog_grammars value 231 Thm.INST_TYPE [Type.alpha |-> ``:Zreg``] boolTheory.COND_RATOR ::
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | numerics.tex | 101 \subsection{The Type of Natural Numbers, {\tt\slshape nat}} 234 \subsection{The Type of Integers, {\tt\slshape int}} 376 \subsection{The Numeric Type Classes}\label{sec:numeric-classes} 390 ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring. 395 function, \cdx{abs}. Type \isa{int} is an ordered ring. 399 An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | numerics.tex | 101 \subsection{The Type of Natural Numbers, {\tt\slshape nat}} 234 \subsection{The Type of Integers, {\tt\slshape int}} 376 \subsection{The Numeric Type Classes}\label{sec:numeric-classes} 390 ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring. 395 function, \cdx{abs}. Type \isa{int} is an ordered ring. 399 An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | Datatype.sml | 43 type hol_type = Type.hol_type 133 val arity = valOf (Type.op_arity {Thy = Thy, Tyop = Tyop}) 135 Type.mk_thy_type {Thy = Thy, Tyop = Tyop, 136 Args = List.tabulate (arity, fn n => Type.alpha)} 880 NONE => hd (Type.decls Tyop) 882 val arity = valOf (Type.op_arity thytyop) 970 acc (Type.type_vars ty)
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | Theory.sml | 27 the "symbol tables" maintained in modules Term and Type). 52 open Feedback Lib Type Term Thm ; 250 * signatures, which are held locally in the Type and Term structures. * 315 fun thy_types thyname = Type.thy_types thyname 367 (Type.prim_new_type {Thy = theory, Tyop = name} arity; thy) 415 (Type.prim_delete_type {Thy = thyname, Tyop = name}; thy) 434 (Type.del_segment s; Term.del_segment s;
|
/seL4-l4v-10.1.1/HOL4/Manual/Guide/ |
H A D | guide.tex | 209 \item Type `{\tt make clean}' to remove all traces of previous executions of 213 \item Type `{\tt make tutorial}' to typeset the \TUTORIAL\ volume using \latex. 215 \item Type `{\tt make all}' to typeset the \TUTORIAL\ volume completely from 239 \item Type `{\tt make clean}' to remove all traces of previous executions of 244 \item Type `{\tt make description}' to typeset the \DESCRIPTION\ volume using 247 \item Type `{\tt make index}' to create the \DESCRIPTION\ index. This creates 250 \item Type `{\tt make all}' to typeset the \DESCRIPTION\ volume completely from 278 \item Type `{\tt make all}' to create the \LaTeX\ sources for the \REFERENCE\ 325 \item Type `{\tt make clean}' to remove all traces of previous executions of 330 \item Type `{\t [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_stepLib.sml | 16 val (Type,Term) = parse_from_grammars arm_stepTheory.arm_step_grammars value 130 val inst_type2 = Thm.INST_TYPE [Type.alpha |-> ``:2``]; 131 val inst_type32 = Thm.INST_TYPE [Type.alpha |-> ``:32``]; 235 val I_flags_fupd = Term.inst [Type.alpha |-> ``:ARMpsr``] combinSyntax.I_tm 515 (Term.inst [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)]
|