/seL4-l4v-10.1.1/HOL4/src/num/reduce/src/ |
H A D | Boolconv.sml | 13 == jrh@cl.cam.ac.uk ==
|
H A D | Arithconv.sml | 13 == mn200@cl.cam.ac.uk ==
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/Serpent/Reference/ |
H A D | Serpent_ReferenceScript.sml | 6 http://www.cl.cam.ac.uk/~rja14/serpent.html
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sml | 756 fun factor' cl = 759 val () = Print.trace LiteralSet.pp "Rule.factor': cl" cl 761 val edges = mk_edges [] [] (LiteralSet.toList cl)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sml | 756 fun factor' cl = 759 val () = Print.trace LiteralSet.pp "Rule.factor': cl" cl 761 val edges = mk_edges [] [] (LiteralSet.toList cl)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/x86/ |
H A D | unix64.S | 87 movzbl %cl, %r10d
|
H A D | darwin64.S | 86 movzbl %cl, %r10d
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
H A D | DerivedBddRules.sml | 851 val cl = value 858 (SPECL (strip_pair(hd cl)) (GENL(strip_pair s)(SPEC_ALL Pth))) 868 (zip (List.take(cl, length cl - 1)) (tl cl)) 871 (SPECL (strip_pair(last cl))
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | selftest.sml | 981 val cl = make_constructorList true [ value 986 (* set_constructorFamily (cl, ``list_REVCASE``) *) 987 val cf = mk_constructorFamily (cl, ``list_REVCASE``, 1041 val cl = make_constructorList false [ value 1045 (* set_constructorFamily (cl, ``tree_red_CASE``) *) 1046 val cf = mk_constructorFamily (cl, ``tree_red_CASE``,
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/poly/ |
H A D | BuildCommand.sml | 454 | BR_ClineK{cline = (_,cl), job_kont = k, ...} => 455 k warn (Systeml.systeml cl)
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/ |
H A D | simpleSexpParseScript.sml | 739 qmatch_assum_rename_tac`_ = FST cl` 740 \\ Cases_on`cl` \\ fs[] \\ var_eq_tac 820 \\ qmatch_assum_rename_tac`FST cl = #" "` 821 \\ Cases_on`cl` \\ fs[] \\ var_eq_tac
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/Serpent/Bitslice/ |
H A D | Serpent_BitsliceScript.sml | 5 http://www.cl.cam.ac.uk/~rja14/serpent.html
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/TEA/ |
H A D | teaScript.sml | 10 (* See http://www.ftp.cl.cam.ac.uk/ftp/papers/djw-rmn/djw-rmn-tea.html *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Intro/document/ |
H A D | root.tex | 12 \texttt{lcp@cl.cam.ac.uk}\\[3ex]
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Intro/document/ |
H A D | root.tex | 12 \texttt{lcp@cl.cam.ac.uk}\\[3ex]
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | PairRules.sml | 178 val ((cl,lt),pl) = int_pairlike p1 x1 value 180 val (c,t) = if cl andalso cr then (true,MK_PAIR(lt,rt)) 181 else if cl 205 val ((cl,lt),pl) = (int_pairlike p1 x'1) value 207 val t = if cl andalso cr then TRANS (MK_PAIR(lt,rt)) th1 208 else if cl
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_FUNCTIONS.sml | 469 | (NONE, cl as (_, n) :: _) => (closureList := (ext, n+1) :: cl; LoadClosure(n+1))
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/test/ |
H A D | tea.sml | 10 (* See http://www.ftp.cl.cam.ac.uk/ftp/papers/djw-rmn/djw-rmn-tea.html *)
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | conv.tex | 529 let FIRST_CONV cl t = 530 itlist $ORELSEC cl NO_CONV t ? failwith `FIRST_CONV`;; 565 let EVERY_CONV cl t = 566 itlist $THENC cl ALL_CONV t ? failwith `EVERY_CONV`
|
H A D | QuantHeuristics.tex | 516 Thomas Tuerk (\url{tt291@cl.cam.ac.uk}). 529 (\url{tt291@cl.cam.ac.uk}), if you have questions.
|
/seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
H A D | quotient.sml | 443 val r'cl = mk_comb{Rator=REL, Rand=r'tm} 444 val rr'cl = mk_comb{Rator=rcl, Rand=r'tm} 445 val req = mk_eq{lhs=rcl, rhs=r'cl} 479 rhs=mk_comb{Rator=cty_ABS, Rand=r'cl}} 877 val r'cl = mk_comb{Rator=REL, Rand=r'tm} 878 val rr'cl = mk_comb{Rator=rcl, Rand=r'tm} 879 val req = mk_eq{lhs=rcl, rhs=r'cl} 901 rhs=mk_comb{Rator=cty_ABS, Rand=r'cl}}
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Induction.sml | 493 val (cl,clauses') = trypluck (match_clause p1) clauses value 494 in cl::match rst clauses'
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | Holmake.sml | 588 | SOME cl => null cl
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | derive_specsLib.sml | 678 val cl = int_to_string (length code) value 679 val str = "Section `"^sec_name^"` consists of "^cl^" instructions."
|
/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | QuantHeuristics.tex | 526 Thomas Tuerk (\url{tt291@cl.cam.ac.uk}). 539 (\url{tt291@cl.cam.ac.uk}), if you have questions.
|