/seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | base.sig | 187 final semantic value resultiing from a parse.
|
/seL4-l4v-master/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | base.sig | 187 final semantic value resultiing from a parse.
|
/seL4-l4v-master/HOL4/examples/temporal_deep/src/examples/ |
H A D | runtime_verificationScript.sml | 415 (* final part *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
H A D | X86CODESIG.sml | 195 (* Code generate operations and construct the final code. *)
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | Graph.sml | 364 (*final declarations of this structure!*)
|
H A D | Table.sml | 466 (*final declarations of this structure!*)
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | functionEncodeLib.sml | 205 val (recrewrites,final) = with_exn dest_imp_only r (nomatch "") 207 val _ = if is_eq final then () else raise (nomatch "the conclusion is not an equality") 209 val target = type_of (lhs final) 210 val _ = (if rall (is_encoded_term o lhs o mimp) (final::stripped) then () else raise Empty) 214 fun supercedes (a,b,c) = can (match_term final) (gf (concl c)) andalso 218 val s = filter supercedes (Net.match (lhs final) (!rewrites)) 223 rewrites := Net.delete (lhs final,ismatch) (!rewrites)) 229 val ffs = filter (can dom_rng o type_of) (free_vars (rand (lhs final))) 250 (map (fn thm' => rewrites := Net.insert (lhs final,(priority:int,name:string,thm')) (!rewrites)) all_thms ; ()) 847 let val (l,final) [all...] |
H A D | acl2encodeLib.sig | 151 (* The final function should be used for definitions which are under *)
|
H A D | polytypicLib.sml | 1751 val final = foldr (fn (a,t) => MATCH_MP MONO_AND (CONJ a t)) (last thms') (butlast thms') value 1752 val rthm = (GEN_ALL (IMP_TRANS final (SPEC var 1753 (ASSUME (mk_forall(var,mk_imp(snd (dest_imp_only (concl final)),conc))))))) 2741 (* removes all hypothesis from the final mutual recursion theorem *) 3121 val final = PURE_REWRITE_RULE [AND_IMP_INTRO,GSYM CONJ_ASSOC] (foldr (uncurry DISCH) (MP inst' (LIST_CONJ (map (fn t => value 3127 if null (hyp final) then final else 3128 raise (mkDebugExn "prove_split_term" ("The exception: " ^ term_to_string (hd (hyp final)) ^ " exists in the final proof!"))
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | tool.tex | 17 fourth and final implementation uses an optimised implementation of 700 \noindent The final step is to use the assumption 748 \noindent Returning to the proof: the final step is now performed by
|
/seL4-l4v-master/HOL4/Manual/Tutorial/ |
H A D | tool.tex | 17 fourth and final implementation uses an optimised implementation of 700 \noindent The final step is to use the assumption 748 \noindent Returning to the proof: the final step is now performed by
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
H A D | stateScript.sml | 64 If ``next (seq n) = NONE`` for some "n" then this final state is repeated
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | Z3_ProofParser.sml | 371 (* Z3 assigns no ID to the final proof step; we use ID 0 *)
|
/seL4-l4v-master/HOL4/tools-poly/poly/ |
H A D | Binaryset.sml | 53 * (sparc) for the final case is very disappointing. Most
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Numerics.sml | 445 val states = length (#final dfa)
|
H A D | regexp_compilerScript.sml | 269 (* regexps, which map to states in the final DFA. The n argument is a *) 827 (* The final definition of the core functionality of the compiler *) 880 (* Definitions that find the accept states and map the final results to *) 1774 (* Well-formedness of final state vector *)
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holmake_types.sml | 192 NONE => (* cut out initial TAB, and final EOF character *)
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | bootup.tex | 192 \texttt{seL4\_Uint8[]} & \texttt{padding} & manual padding so final struct is a multiple of the word size \\
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/ |
H A D | Recftn.sml | 735 val final = new_specification value 741 final
|
/seL4-l4v-master/HOL4/src/tfl/src/ |
H A D | RW.sml | 444 * by variants. The final pairs are returned. 604 (* that has function syntax. This will allow the final *)
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibMeson.sml | 531 val () = assert (length proof = length g) (Bug "meson: bad final state")
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Parse_support.sml | 479 the basis for calculating the bound vars in the final
|
/seL4-l4v-master/HOL4/src/portableML/poly/concurrent/ |
H A D | Future.sml | 642 (*final declarations of this structure!*)
|
/seL4-l4v-master/HOL4/src/unwind/Manual/ |
H A D | description.tex | 17 \ml{PRUNE}. The final group of functions combine unfolding, unwinding and
|
/seL4-l4v-master/HOL4/examples/CCS/ |
H A D | CoarsestCongrScript.sml | 830 (* Part 5: final check *)
|