/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Z3_ProofReplay.sml | 920 else if !Library.trace > 2 then 1063 if !Library.trace > 2 then 1081 val _ = if !Library.trace > 1 then
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | normalForms.sml | 279 convs = [{name = "extensionality simplification", trace = 2, 1033 [{name = "conditional lifting at rand", trace = 2, 1094 [{name = "COND_SIMP_CONV", trace = 2,
|
H A D | mlibRewrite.sml | 41 fun chat s = (trace s; true)
|
H A D | mlibTermorder.sml | 38 fun chat s = (trace s; true)
|
H A D | mlibUseful.sml | 86 val trace = Lib.say; value
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | selftest.sml | 91 trace ("types", 1) term_to_string t1 ^ " - " ^ 92 trace ("types", 1) term_to_string t2 ^ 209 case Lib.total (trace ("show_typecheck_errors", 0) Parse.Term) [QUOTE s] of
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | polytypicLib.sml | 27 (* wrapException adds a name to the trace in an exception and *) 28 (* wrapExceptionHOL adds a name to the trace then converts to a HOL_ERR *) 66 (* Prints a function trace *) 86 fun wrapException name (polyExn(level,trace,msg)) = raise polyExn(level,name::trace,msg) 98 | wrapExceptionHOL name (polyExn(level,trace,msg)) = 100 (mk_HOL_ERR "polyLib" (last trace) (set_level level msg)) (name::(butlast trace))) 130 handle (polyExn(level,trace,msg)) => wrapException "guarenteed" (polyExn(Debug,trace,ms [all...] |
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | ConseqConv.sig | 8 trace "DEPTH_CONSEQ_CONV" can be used to get debug information
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | selftest.sml | 390 case Lib.total (trace("show_typecheck_errors", 0) Parse.Term)
|
/seL4-l4v-10.1.1/HOL4/src/emit/ |
H A D | EmitML.sml | 828 trace ("Greek tyvars",0) 1466 (trace ("Unicode",0) 1517 S " fun typ s = Feedback.trace(\"Vartype Format Complaint\", 0)\n\ 1585 Feedback.trace ("Unicode", 0)
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | bitstringLib.sml | 25 fun qm l = Feedback.trace ("metis", 0) (metisLib.METIS_TAC l)
|
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | lalr.sml | 390 be propagated. For each rule, it must trace the shift/gotos in the LR(0)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_Lib.sml | 17 { name = tm_name, trace = 3, key = SOME ([],tm), conv = K (K EVAL) };
|
H A D | x86_decoderScript.sml | 450 { name = tm_name, trace = 3, key = SOME ([],tm), conv = K (K EVAL) }; 452 val if_ss = conv_ss { name = "if", trace = 3,
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_Lib.sml | 19 { name = tm_name, trace = 3, key = SOME ([],tm), conv = K (K EVAL) };
|
H A D | x64_decoderScript.sml | 596 { name = tm_name, trace = 3, key = SOME ([],tm), conv = K (K EVAL) }; 598 val if_ss = conv_ss { name = "if", trace = 3,
|
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/ |
H A D | prob_diceScript.sml | 57 name = "DDG_INDEP_FN_CONV", trace = 10}],
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | CCSConv.sml | 34 val trace = fn : bool -> unit
|
/seL4-l4v-10.1.1/HOL4/examples/PSL/regexp/ |
H A D | regexpTools.sml | 24 * The trace levels of the regular expression library:
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/small-step/ |
H A D | forSmallScript.sml | 745 (*trace for e1*) 810 (*Need a handle wrapper around rest of trace*)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | utilsLib.sml | 474 fun qm l = Feedback.trace ("metis", 0) (metisLib.METIS_PROVE l) 475 fun qm_tac l = Feedback.trace ("metis", 0) (metisLib.METIS_TAC l)
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Induction.sml | 187 val quiet_metis = Feedback.trace ("metis", 0) (metisLib.METIS_PROVE []) 188 val quiet_meson = Feedback.trace ("meson", 0) (BasicProvers.PROVE [])
|
H A D | RW.sml | 687 trace ("assumptions", 1) 695 trace ("assumptions", 1)
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Print.sml | 1554 fun trace ppX nameX x = function 1555 Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Print.sml | 1554 fun trace ppX nameX x = function 1555 Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
|