| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Useful.sml | 68 fun trace mesg = !tracePrint mesg; function
|
| /seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/small-step/ |
| H A D | for_osmallScript.sml | 983 (*trace for e1*)
1048 (*Need a handle wrapper around rest of trace*)
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | wordsLib.sml | 589 trace = 3,
664 val NEG_EQ_0 = trace ("metis", 0) (METIS_PROVE [WORD_NEG_MUL, WORD_NEG_EQ_0])
2634 fun save x = Feedback.trace ("Theory.save_thm_reporting", 0) save_thm x
|
| H A D | blastLib.sml | 1055 val FCP_NEQ = trace ("metis",0) prove(
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Pmatch.sml | 453 trace ("Unicode", 0) Parse.term_to_string t^
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | folMapping.sml | 34 fun chat s = (trace s; true)
|
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | patternMatchesLib.sml | 149 trace = 2,
156 trace = 2,
163 trace = 2,
1669 trace = 2,
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | derive_specsLib.sml | 59 There's a bug in the trace generation to do with guards that are not
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | arm_stepLib.sml | 872 val lem1 = trace ("metis",0) (METIS_PROVE [WORD_EQ_ADD_RCANCEL])
|
| /seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
| H A D | DerivedBddRules.sml | 820 val _ = print "Computing trace: "
|
| H A D | PrimitiveBddRules.sml | 90 (* Setup trace variable for controlling debug output *)
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | muSyntax.sml | 350 However, we'll need to fix the trace generation code before formulas like that can be traced *)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | mechReasoning.sml | 40 trace = 2,
|
| /seL4-l4v-10.1.1/HOL4/src/IndDef/Manual/ |
| H A D | paper.tex | 867 trace and transition semantics for a simple process algebra, \mbox{together}
|
| /seL4-l4v-10.1.1/HOL4/src/list/src/ |
| H A D | ListConv1.sml | 347 (* trace of the exception handling is possible. We also include *)
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
| H A D | vars_as_resourceFunctor.sml | 2022 trace = 2}
2026 trace = 2}
3838 (map (fn c => {conv = K (K c), key = NONE, name = "user-conversion", trace = 2}) convL),
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | mechReasoning.sml | 72 trace = 2,
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/ |
| H A D | ind_types.sml | 1517 |> trace ("Vartype Format Complaint", 0)
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | term_grammar.sml | 1330 trace ("types", 1) (tmprint (strip_overload_info G)) t
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | libraries.tex | 2712 trace: int,
2718 I campo \ml{name} e \ml{trace} sono usati quando il tracing del semplificatore
2720 semplificatore � maggiore di o uguale al campo \ml{trace}, allora sar�
3380 - Feedback.trace ("word printing", 1) Parse.print_term ``32w``;
|
| /seL4-l4v-10.1.1/HOL4/examples/CCS/ |
| H A D | ContractionScript.sml | 1623 (* OBS_contracts and trace *)
|
| /seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/ |
| H A D | ModelLemmasScript.sml | 253 (* AUTOMATON_PATH A w <=> w is a (finite or infinite) trace of A *)
|
| /seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
| H A D | Defn.sml | 445 fun save x = Feedback.trace ("Theory.save_thm_reporting", 0) save_thm x
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootLib.sml | 2513 trace = 2}
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
| H A D | CODEGEN_PARSETREE.sml | 1575 (* Get a name for any functions. This is used for profiling and exception trace. *)
|