Searched refs:triple (Results 1 - 25 of 47) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DtripleSyntax.sml12 HolKernel.syntax_fns4 "triple" "TRIPLE"
15 HolKernel.syntax_fns3 "triple" "case_sum"
H A DtripleScript.sml4 val _ = new_theory "triple";
9 (* we define a total-correctness machine-code Hoare triple *)
28 (* theorems about this Hoare triple *)
H A DtripleLib.sml7 val ERR = Feedback.mk_HOL_ERR "triple"
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/
H A Dbuild-ios.sh13 local triple=$4
20 ../configure --host=${triple} && make
H A Dgenerate-ios-source-and-headers.py46 triple = 'i386-apple-darwin10' variable in class:simulator_platform
56 triple = 'arm-apple-darwin10' variable in class:device_platform
132 subprocess.check_call(['../configure', '-host', platform.triple], env=env)
H A Dgenerate-osx-source-and-headers.py41 triple = 'i386-apple-darwin10' variable in class:desktop_platform_32
51 triple = 'x86_64-apple-darwin10' variable in class:desktop_platform_64
125 subprocess.check_call(['../configure', '-host', platform.triple], env=env)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DUTuple.sml12 fun triple x y z = (x,y,z) function
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DUTuple.sml12 fun triple x y z = (x,y,z) function
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/
H A DUTuple.sml12 fun triple x y z = (x,y,z) function
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/
H A DcompilerLib.sig13 returns a Hoare triple containing the generated code *)
/seL4-l4v-10.1.1/HOL4/src/compute/examples/
H A DSort.sml48 fun triple l () = let val ll = l() in ll@(ll@ll) end; function
55 val L1200 = triple L400;
H A DMergeSort.sml30 val triple_def = Define_rw ` triple l = append l (append l l) `
104 val L1200_def = Define_rw ` L1200 = triple L400 `;
/seL4-l4v-10.1.1/HOL4/src/emit/
H A DConstMapML.sml161 of SOME triple => triple
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DGenPolyCanon.sml15 r_asscomm : thm (* swaps 1 and 2 in r-associated triple *),
16 l_asscomm : thm (* swaps 2 and 3 in l-associated triple *),
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_seq_monadScript.sml728 (\memaddrdesc. let triple = (memaddrdesc.paddress,ii,size) in
734 (monitor.MarkExclusiveGlobal triple)
735 (\u. monitor.MarkExclusiveLocal triple)
737 monitor.MarkExclusiveLocal triple)
750 let triple = (memaddrdesc.paddress,ii,size) in
752 seqE (monitor.IsExclusiveLocal triple)
756 seqE (monitor.IsExclusiveGlobal triple)
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/
H A Darm_seq_monadScript.sml734 (\memaddrdesc. let triple = (memaddrdesc.paddress,ii,size) in
740 (monitor.MarkExclusiveGlobal triple)
741 (\u. monitor.MarkExclusiveLocal triple)
743 monitor.MarkExclusiveLocal triple)
756 let triple = (memaddrdesc.paddress,ii,size) in
758 seqE (monitor.IsExclusiveLocal triple)
762 seqE (monitor.IsExclusiveGlobal triple)
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/
H A Dexport_theory.scala193 triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
206 triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body)
309 list(triple(string, list(sort), string))(body)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/
H A Dexport_theory.scala193 triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
206 triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body)
309 list(triple(string, list(sort), string))(body)
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/
H A DregexpLib.sml140 val triple = rhs (concl compile_thm) value
141 val [t1,t2,t3] = strip_pair triple
/seL4-l4v-10.1.1/HOL4/examples/machine-code/acl2/
H A Dm1_progLib.sml13 (* m1_spec produces Hoare triple theorems for M1 instructions *)
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/
H A Drules.tex793 f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\
794 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
807 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ (f\ x)
813 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ (f\ x)\ (f\ x)
820 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ x\ (f\ x)
825 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/
H A Drules.tex793 f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\
794 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
807 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ (f\ x)
813 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ (f\ x)\ (f\ x)
820 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ x\ (f\ x)
825 \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\
[all...]
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DPortable.sig30 val triple : 'a -> 'b -> 'c -> 'a * 'b * 'c value
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A DLib.sig151 val triple : 'a -> 'b -> 'c -> 'a * 'b * 'c value
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/
H A Dshrink.sml48 It returns a triple consisting of:

Completed in 199 milliseconds

12