/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | tripleSyntax.sml | 12 HolKernel.syntax_fns4 "triple" "TRIPLE" 15 HolKernel.syntax_fns3 "triple" "case_sum"
|
H A D | tripleScript.sml | 4 val _ = new_theory "triple"; 9 (* we define a total-correctness machine-code Hoare triple *) 28 (* theorems about this Hoare triple *)
|
H A D | tripleLib.sml | 7 val ERR = Feedback.mk_HOL_ERR "triple"
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | build-ios.sh | 13 local triple=$4 20 ../configure --host=${triple} && make
|
H A D | generate-ios-source-and-headers.py | 46 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 D | generate-osx-source-and-headers.py | 41 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 D | UTuple.sml | 12 fun triple x y z = (x,y,z) function
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | UTuple.sml | 12 fun triple x y z = (x,y,z) function
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | UTuple.sml | 12 fun triple x y z = (x,y,z) function
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | compilerLib.sig | 13 returns a Hoare triple containing the generated code *)
|
/seL4-l4v-10.1.1/HOL4/src/compute/examples/ |
H A D | Sort.sml | 48 fun triple l () = let val ll = l() in ll@(ll@ll) end; function 55 val L1200 = triple L400;
|
H A D | MergeSort.sml | 30 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 D | ConstMapML.sml | 161 of SOME triple => triple
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | GenPolyCanon.sml | 15 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 D | arm_seq_monadScript.sml | 728 (\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 D | arm_seq_monadScript.sml | 734 (\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 D | export_theory.scala | 193 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 D | export_theory.scala | 193 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 D | regexpLib.sml | 140 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 D | m1_progLib.sml | 13 (* m1_spec produces Hoare triple theorems for M1 instructions *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | rules.tex | 793 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 D | rules.tex | 793 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 D | Portable.sig | 30 val triple : 'a -> 'b -> 'c -> 'a * 'b * 'c value
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | Lib.sig | 151 val triple : 'a -> 'b -> 'c -> 'a * 'b * 'c value
|
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | shrink.sml | 48 It returns a triple consisting of:
|