/seL4-l4v-10.1.1/HOL4/src/monad/more_monads/ |
H A D | selftest.sml | 84 val _ = unicode_off (raw_backend (trace ("types", 1) testutils.tpp))
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/ |
H A D | HexSolitaireScript.sml | 200 (* Print out a trace as found by findTrace *)
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Print.sig | 202 val trace : 'a pp -> string -> 'a -> unit value
|
H A D | Useful.sig | 27 val trace : string -> unit value
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Print.sig | 202 val trace : 'a pp -> string -> 'a -> unit value
|
/seL4-l4v-10.1.1/HOL4/src/IndDef/ |
H A D | CoIndDefLib.sml | 196 |> trace ("syntax_error", 0) 197 |> trace ("show_typecheck_errors", 0)
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | selftest.sml | 129 val _ = trace ("types", 1) tpp "case (p :'a # 'b) of (x,y) => x" 134 val _ = trace ("types", 1) tpp "if (b :bool) then (x :'a) else (y :'a)"
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | intSimps.sml | 156 val _ = trace (5, LZ_TEXT (fn () => "Trying cached arithmetic d.p. on "^ 165 trace(1,PRODUCE(tm,DPname,thm)); thm
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | inst_logic.py | 19 from target_objects import functions, trace, pairings, pre_pairings, printout namespace
|
H A D | trace_refute.py | 20 from target_objects import functions, trace, pairings, symbols, printout namespace 201 """we're getting call addresses from the binary trace, and using the 216 trace ('failed to find Call node near %s' % init_n) 406 trace ("Loop in %s non-uniform, additional entries %s." 410 trace ("Loop in %s non-uniform, inner loop." % fname)
|
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | EmitTeX.sml | 372 val trace = Feedback.trace value 376 val PT = Parse.mlower o (PT0 |> trace ("types", 0)) 508 fun UnicodeOff f = trace ("Unicode", 0) f 550 |> trace ("pp_dollar_escapes", 0)
|
H A D | selftest.sml | 97 val s = trace ("EmitTeX: print datatypes compactly", 1)
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | muCheck.sml | 808 then ref (SOME []) else ce (*turn on witness trace if existential mf*) 830 (* given the list of top-level approximations, find a path through them and return it as a trace *) 832 (* FIXME: a more readable trace would only print out those AP's that are talked about in the corresponding property *) 866 fun mk_tr (apx::trl) prev = (* trace out a path of transitions over trbl *) 883 in (*next state on the trace*) 895 val trace = List.map (pt_bdd2state state vmc) tr value 896 val _ = List.app (dbgTools.DTM (dpfx^"mt_trace")) trace(*DBG*) 897 in trace end 954 OUT: termbdd of set of states satisfying mf, success theorem, ce/witness trace, cache of reusable stuff *) 965 val trace value 976 val trace = if Option.isSome (!ce) value 987 val trace = makeTrace mf state vm mu_init_data ce (valOf Itb) value [all...] |
H A D | commonTools.sml | 49 trace=2, 57 trace=2, 65 trace=2,
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | subtypeTools.sml | 257 and trace = 2 value 259 {name = name, key = key, conv = conv, trace = trace}
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Z3_ProofParser.sml | 308 val _ = if !Library.trace > 0 andalso 389 val _ = if !Library.trace > 1 then 395 val _ = if !Library.trace > 0 then
|
/seL4-l4v-10.1.1/HOL4/src/q/ |
H A D | Q.sml | 30 fun TC_OFF f x = trace ("show_typecheck_errors", 0) f x 368 f |> trace ("notify type variable guesses", 0) 369 |> trace ("show_typecheck_errors", 0)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/ |
H A D | boolTools.sml | 269 trace = 2, 274 trace = 2, 279 trace = 2,
|
/seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
H A D | QbfCertificate.sml | 349 val _ = if !QbfTrace.trace < 1 orelse HOLset.isEmpty (Thm.hypset thm) then 353 val _ = if !QbfTrace.trace < 1 orelse Term.aconv (Thm.concl thm) t then 429 val _ = if !QbfTrace.trace < 1 orelse 435 val _ = if !QbfTrace.trace < 1 orelse
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibSubsume.sml | 43 fun chat s = (trace s; true)
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | testutils.sml | 91 fun unicode_off f = Feedback.trace ("Unicode", 0) f
|
/seL4-l4v-10.1.1/HOL4/src/proofman/tests/ |
H A D | selftest.sml | 124 |> trace ("Unicode", 0))
|
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/ |
H A D | res_quanLib.sml | 430 name = "RES_FORALL_CONV", trace = 2}, 433 name = "RES_EXISTS_CONV", trace = 2}, 436 name = "RES_SELECT_CONV", trace = 2}, 439 name = "RES_EXISTS_UNIQUE_CONV", trace = 2}],
|
/seL4-l4v-10.1.1/HOL4/src/string/ |
H A D | stringLib.sml | 159 Feedback.trace ("Define.storage_message", 0)
|
/seL4-l4v-10.1.1/HOL4/examples/miller/formalize/ |
H A D | numContext.sml | 37 fun trace l s = if l > !trace_level then () else say (s ^ "\n"); function
|