| /seL4-l4v-10.1.1/HOL4/src/tfl/src/test/ |
| H A D | pattern_matchingScript.sml | 9 val def = Hol_defn; value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/test/ |
| H A D | regAllocTest.sml | 16 val def = (SSA_RULE o normalize) fact_def; value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/examples/ |
| H A D | simple_examples.sml | 151 val def = Define `f (x1:word32) = if (x1 = 0w) then x1 else (x1+1w)` value
152 val def = Define `f (x1:word32) = if (x1 < 0w) then x1 else (x1+1w)` value
153 val def = Define `f (x1:word32) = if (x1 <= 0w) then x1 else (x1+1w)` value
154 val def = Define `f (x1:word32) = if (x1 <+ 0w) then x1 else (x1+1w)` value
155 val def = Define `f (x1:word32) = if (x1 <=+ 0w) then x1 else (x1+1w)` value
156 val def = Define `f (x1:word32) = if ($> x1 0w) then x1 else (x1+1w)` value
157 val def = Define `f (x1:word32) = if (x1 >= 0w) then x1 else (x1+1w)` value
158 val def = Define `f (x1:word32) = if (x1 >+ 0w) then x1 else (x1+1w)` value
159 val def = Define `f (x1:word32) = if (x1 >=+ 0w) then x1 else (x1+1w)` value
168 val def = Define ` value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/opentheory/compat/ |
| H A D | HOL4boolScript.sml | 79 val def = new_definition("literal_case_def",concl boolTheory.literal_case_DEF) value
88 val def = new_definition("LET",concl boolTheory.LET_DEF) value
97 val def = new_definition("TYPE_DEFINITION",concl boolTheory.TYPE_DEFINITION) value
|
| /seL4-l4v-10.1.1/HOL4/src/search/ |
| H A D | bftScript.sml | 44 val def = (* Define function and prove termination *) value
|
| H A D | dftScript.sml | 44 val def = (* Define function and prove termination *) value
|
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/examples/calculator/ |
| H A D | hashtbl.h | 21 void *def; member in class:hashData
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
| H A D | x64_compilerLib.sml | 119 val def = RW [] (foldr (uncurry CONJ) TRUTH defs) value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
| H A D | compiler.sml | [all...] |
| H A D | defunctionalize.sml | 442 val def = Defn.eqns_of (Defn.Hol_defn "x" `^spec`) value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/examples/ |
| H A D | arm_compiler_demoScript.sml | 42 val def = Define q value
|
| /seL4-l4v-10.1.1/HOL4/src/IndDef/ |
| H A D | IndDefLib.sml | 198 val def as (def_t,_) = parse q value
|
| H A D | CoIndDefLib.sml | 198 val def as (def_t, _) = parse q value
|
| /seL4-l4v-10.1.1/HOL4/src/finite_map/ |
| H A D | flookupLib.sml | 215 val def = Definition.new_definition (s, boolSyntax.mk_eq (v, t)) value
|
| /seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/ |
| H A D | Opentheory.sml | 179 val def = define_const c t value
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/ |
| H A D | Table.sml | 220 fun def Empty = false function
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_bigopsScript.sml | 815 val def = Define [ANTIQUOTE (mk_eq(mk_comb(name,input),c))] value
|
| H A D | lisp_correctnessScript.sml | 376 val def = abbrev_code_for_compile_inst_def value
381 val def = abbrev_code_for_compile_def value
386 val def = abbrev_code_for_print_def value
391 val def = abbrev_code_for_equal_def value
396 val def = abbrev_code_for_cons_def value
401 val def = abbrev_code_for_parse_def value
[all...] |
| H A D | lisp_initScript.sml | 64 val def = new_definition("init_func",mk_eq(lhs_tm,f_tm)) value
73 val def = CONJ def pre value
|
| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/ |
| H A D | modelCheckLib.sml | 263 val def = bdd_to_definition b; value
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | pexport.cpp | 320 SpaceAlloc::SpaceAlloc(bool isMut, POLYUNSIGNED def) argument
|
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/ |
| H A D | c_outputLib.sml | 457 val def = SPEC_ALL def; value
481 val def = normalise_fun_def def false; value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
| H A D | Recftn.sml | 754 val def = value
770 val def = value
784 val def = value
798 val def = value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
| H A D | compilerLib.sml | 119 val def = RW [] (foldr (uncurry CONJ) TRUTH defs) value
241 val (def,pre) = tailrec_define_with_pre tm pre_tm value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
| H A D | MachineTransitionScript.sml | 610 val def = EQ_MP (MK_EXISTS(Q.GEN `rep` th2)) th1 value
|