/seL4-l4v-10.1.1/HOL4/src/compute/src/ |
H A D | clauses.sml | 308 fun db_of_entry (ss, r) = let val (db,opt) = !r in db end 339 fun db_of_entry (ss, r) = let val (db,opt) = !r in (ss,db) end
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/ |
H A D | for_compileScript.sml | 205 ���(option_CASE opt n s = v) ��� 206 opt = NONE ��� n = v ��� ���sv. opt = SOME sv ��� s sv = v���, 207 Cases_on ���opt��� >> simp[]);
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | selftest.sml | 18 val _ = tpp "case opt of NONE => T | SOME b => b"
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_random_testingLib.sml | 721 fun arm_step_updates opt opc = let 722 val tm = opc |> try (armLib.arm_step opt) 734 val opt = String.concat [arch, ", ", block, ", ", value 740 val (l,r) = case arm_step_updates opt opc
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | rich_text_area.scala | 144 opt <- List(old_text_info, new_text_info) 145 (_, Text.Info(r1, _)) <- opt
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | rich_text_area.scala | 144 opt <- List(old_text_info, new_text_info) 145 (_, Text.Info(r1, _)) <- opt
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | Window.sml | 198 fun ShowWindow (win, opt) = 201 case opt of
|
/seL4-l4v-10.1.1/HOL4/src/datatype/record/ |
H A D | RecordType.sml | 96 fun update_tyinfo opt new_simpls tyinfo = 102 case opt of
|
/seL4-l4v-10.1.1/HOL4/src/num/termination/ |
H A D | TotalDefn.sml | 554 val (defn',opt) = 563 ; (LIST_CONJ (map GEN_ALL (eqns_of defn')), ind_of defn', opt)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | completion.scala | 299 underscores ~ word2 ~ opt("?") ^^
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Isar/ |
H A D | token.scala | 74 val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | completion.scala | 299 underscores ~ word2 ~ opt("?") ^^
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Isar/ |
H A D | token.scala | 74 val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/cbv-lc/ |
H A D | optScript.sml | 13 val _ = new_theory "opt";
|
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Term.sml | 622 fun list_mk_binder opt = 623 let val f = check_opt opt 697 fun strip_binder opt = 699 case opt of
|
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | pydot.py | 456 def RegOpenKeyEx(key, subkey, opt, sam): 458 ctypes.windll.advapi32.RegOpenKeyExA(key, subkey, opt, sam, ctypes.byref(result)) 558 '/opt/local/bin', 559 '/opt/bin', '/sw/bin', '/usr/share',
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | ltmain.sh | 1588 # opt=$1; shift 1589 # case $opt in 3976 for opt in "$nonopt" ${1+"$@"} 3978 if test -d "$opt"; then 3979 func_append libdirs " $opt" 3981 elif test -f "$opt"; then 3982 if func_lalib_unsafe_p "$opt"; then 3983 func_append libs " $opt" 3985 func_warning "'$opt' is not a valid libtool archive" 3989 func_fatal_error "invalid argument '$opt'" [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | windows_specific.cpp | 1120 unsigned opt = get_C_unsigned(taskData, DEREFWORDHANDLE(args)->Get(2)); local 1127 opt ? REG_OPTION_NON_VOLATILE : REG_OPTION_VOLATILE,
|
/seL4-l4v-10.1.1/HOL4/polyml/ |
H A D | ltmain.sh | 1588 # opt=$1; shift 1589 # case $opt in 3976 for opt in "$nonopt" ${1+"$@"} 3978 if test -d "$opt"; then 3979 func_append libdirs " $opt" 3981 elif test -f "$opt"; then 3982 if func_lalib_unsafe_p "$opt"; then 3983 func_append libs " $opt" 3985 func_warning "'$opt' is not a valid libtool archive" 3989 func_fatal_error "invalid argument '$opt'" [all...] |
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | Sequents.tex | 63 One could opt to represent sequences as first-order objects (such as
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
H A D | Sequents.tex | 63 One could opt to represent sequences as first-order objects (such as
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | utilsLib.sml | 122 fun process_opt opt = process_option (Lib.C Lib.mem (List.concat opt)) 123 (fn option => find_pos (Lib.mem option) opt)
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | lzConv.sml | 347 fun STRIP_BINDER_CONV opt conv tm = let 348 val (vlist,M) = strip_binder opt tm 350 GEN_ABS opt vlist (conv M) 366 val (_, M') = strip_binder opt rhs (* v = Bvar *) 367 val eq_thm' = GEN_ABS opt gvs (conv M')
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | sessions.scala | 793 option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^ 823 (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/ |
H A D | sessions.scala | 793 option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^ 823 (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
|