| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | pseudo_compile.py | 25 from target_objects import symbols, trace namespace
306 trace ('Compiling in %s.' % function.name)
|
| /seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
| H A D | ho_basicTools.sml | 45 fun trace l s = if l > !trace_level then () else say (s ^ "\n"); function
|
| /seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
| H A D | posrealTools.sml | 137 trace = 2, key = SOME ([],rat_reduce_pat)}],
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/ |
| H A D | arm_emitScript.sml | 139 fun f x = [QUOTE (trace ("Unicode",0) EmitTeX.datatype_thm_to_string x)]
|
| /seL4-l4v-10.1.1/HOL4/examples/Crypto/MARS/ |
| H A D | MARSScript.sml | 228 {name="PBETA",trace = 3,conv=K (K PairRules.PBETA_CONV),
|
| /seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/KatiPuzzle/ |
| H A D | KatiPuzzleScript.sml | 221 (* Print out a trace as found by traceBack *)
|
| /seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/ |
| H A D | SolitaireScript.sml | 245 (* Print out a trace as found by findTrace *)
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | functionEncodeLib.sig | 5 val trace : int -> string -> unit value
|
| H A D | tutorial.ml | 134 (* The rewrite names are displayed in the trace as, in this case, R(listnum) *)
232 (* By setting the trace level to 3 we can see that the back-chaining *)
731 (* In the trace, the steps of the translation are described as follows: *)
|
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | SmtLib_Parser.sml | 553 val _ = if !Library.trace > 1 then
560 val _ = if !Library.trace > 0 then
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/poly/concurrent/ |
| H A D | Future.sml | 198 if ! Multithreading.trace >= 2 then
265 if tick andalso ! status_ticks mod (if ! Multithreading.trace >= 1 then 2 else 10) = 0
|
| /seL4-l4v-10.1.1/HOL4/examples/miller/subtypes/ |
| H A D | subtypeTools.sml | 43 fun trace l s = if l > !trace_level then () else say (s ^ "\n"); function
573 val _ = trace 2
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
| H A D | vars_as_resourceBaseFunctor.sml | 774 trace = 2},
777 trace = 2}])
|
| /seL4-l4v-10.1.1/HOL4/examples/CCS/ |
| H A D | TraceScript.sml | 385 (* The trace relation *)
397 val _ = type_abbrev ("trace",
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Formula.sml | 587 val () = Print.trace pp "Formula.splitGoal: fm" fm
588 val () = Print.trace (Print.ppList pp) "Formula.splitGoal: result" result
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Formula.sml | 587 val () = Print.trace pp "Formula.splitGoal: fm" fm
588 val () = Print.trace (Print.ppList pp) "Formula.splitGoal: result" result
|
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
| H A D | elliptic_exampleScript.sml | 364 trace = 2,
|
| H A D | ellipticScript.sml | 187 and trace = 2
189 {name = name, key = key, conv = conv, trace = trace}
|
| /seL4-l4v-10.1.1/HOL4/src/list/src/ |
| H A D | listSimps.sml | 331 trace = 2,
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibSolver.sml | 33 fun chat s = (trace s; true)
|
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | patternMatchesSyntax.sig | 171 Whether it is use can be controled via the trace
|
| /seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/parser/ |
| H A D | ParserTools.sml | 50 * Set the trace level of the regular expression library:
|
| /seL4-l4v-10.1.1/HOL4/src/basicProof/ |
| H A D | BasicProvers.sml | 345 val a = trace ("syntax_error", 0) Parse.Absyn q
357 val tm = trace ("show_typecheck_errors", 0)
684 trace = 2, name = "ABBREV_CONV"}],
|
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | misc.tex | 12 \item The trace system for controlling feedback and printing.
77 The trace system gives the user one central interface with which to control most of \HOL's many different flags, though they be scattered all over the system, and defined in different modules.
79 For example, a trace level of zero will usually make a tool remain completely
91 trace : (string * int) -> ('a -> 'b) -> ('a -> 'b)
96 The \ml{set\_trace} function allows the user to set a trace directly.
98 Finally, the \ml{trace} function allows for a trace to be temporarily set while a function executes, restoring the trace to its old value when the function returns (whether normally, or with an exception).
1046 If the trace \texttt{EmitTeX:~print~datatypes~compactly} is set to 1 (see the \texttt{tr} option below) the description is printed in a more compact form.
1146 (In interactive HOL, the token-merging analysis is controlled by a trace variabl
[all...] |
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | misc.tex | 12 \item The trace system for controlling feedback and printing.
77 The trace system gives the user one central interface with which to control most of \HOL's many different flags, though they be scattered all over the system, and defined in different modules.
79 For example, a trace level of zero will usually make a tool remain completely
91 trace : (string * int) -> ('a -> 'b) -> ('a -> 'b)
96 The \ml{set\_trace} function allows the user to set a trace directly.
98 Finally, the \ml{trace} function allows for a trace to be temporarily set while a function executes, restoring the trace to its old value when the function returns (whether normally, or with an exception).
1052 (In interactive HOL, the token-merging analysis is controlled by a trace variable called \texttt{"pp\_avoids\_symbol\_merges"}.)
1110 Causes the term or theorem to be printed with the \texttt{types} trace se
[all...] |