/seL4-l4v-master/HOL4/examples/hardware/hol88/ |
H A D | PARITY.ml | 19 "!in out. 20 (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~(out t) | out t)) 22 (!t. out t = PARITY t in)", 30 (`ONE_DEF`, "ONE(out:num->bool) = !t. out t = T");; 34 (`NOT_DEF`, "NOT(in,out:num->bool) = !t. out [all...] |
H A D | Stokes.ml | 12 "(COUNTER 0 reset out = T) /\ 13 (COUNTER (SUC m) reset out = 15 ((out(SUC m) = ((reset m=0) => 0 | (out m)+1)) /\ 16 COUNTER m reset out)))");; 27 "(INC 0 out p1 = T) /\ 28 (INC (SUC m) out p1 = 29 (p1(SUC m) = out(SUC m)+1) /\ 30 INC m out p1)");; 34 "(DEL 0 p2 (out [all...] |
/seL4-l4v-master/HOL4/examples/parity/ |
H A D | PARITYScript.sml | 23 ``!inp out. 24 (out 0 = T) /\ 25 (!t. out (SUC t) = if inp (SUC t) then ~out t else out t) 27 !t. out t = PARITY t inp``, 34 val ONE_def = Define `ONE(out:num->bool) = !t. out t = T`; 36 val NOT_def = Define `NOT(inp, out:num->bool) = !t. out [all...] |
H A D | PARITY_exercisesScript.sml | 10 RESET_REG(reset,inp,out) = 11 (!t. reset t ==> (out t = T)) /\ 12 (!t. out (t + 1) = if reset t \/ reset (t + 1) then T else inp t) 16 RESET_REG_IMP (reset,inp,out) = 21 MUX(mo,mo,ro2,out) 30 ``RESET_REG_IMP(reset,inp,out) ==> 31 RESET_REG(reset,inp,out)``, 39 The value at out is T if and only if there have been an even 44 RESET_PARITY (reset,inp,out) <=> 45 (out [all...] |
/seL4-l4v-master/HOL4/examples/dev/Fact32/ |
H A D | NOT32.ml | 4 `NOT32(inp,out) = !t. out t = ~(inp t : word32)`; 9 ``COMB ($~:word32->word32) (inp, out) = NOT32(inp,out)``, 17 ``NOT32(inp,out) 19 NOT32(inp at clk,out at clk)``, 26 \module NOT32 (inp,out);\n\ 29 \ output [size:0] out;\n\ 31 \ assign out = ~inp;\n\ 37 fun NOT32vInst (out [all...] |
H A D | exor32.ml | 21 `XOR32(in1:num->word32,in2,out) = !t. out t = (in1 t) ?? (in2 t)`; 31 ``COMB (UNCURRY $??) (in1 <> in2, out) = XOR32(in1,in2,out)``, 39 ``XOR32(in1,in2,out) 41 XOR32(in1 at clk,in2 at clk,out at clk)``, 52 (* instances) and a function to print a HOL term ``XOR32(in1,in2,out)`` as *) 53 (* an instance, using the type of ``out`` to compute the word width *) 59 \module XOR32 (in1,in2,out);\n\ 62 \ output [size:0] out;\ [all...] |
/seL4-l4v-master/HOL4/examples/Hoare-for-divergence/ |
H A D | while_langScript.sml | 30 output_of ((s,out):state) = out 34 subst n e (s,out) = ((n =+ e s) s,out:value list) 38 print e ((s,out):state) = (s,out ++ [e s]) 42 guard x ((s,out):state) = (x s ��� 0) 76 output = LUB { fromList out | ���q t. RTC step (p,s) (q,t,out) }
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | HOLPage.sml | 51 fun out s = TextIO.output(os, s) function 53 app out ["<A HREF=\"file://", target, "\">", anchor, "</A>"] 85 ; out " \n" 94 out "<HTML>\ 96 out "<BODY BGCOLOR=\""; out bgcolor; out "\">\n"; 97 out "<H1>HOL Reference Page</H1>\n"; 99 out "<DL>"; 101 out"<D [all...] |
H A D | Doc2Html.sml | 87 fun out s = TextIO.output(ostrm,s) function 89 fun markout PARA = out "\n<P>\n" 91 (out "<SPAN class = \"TEXT\">"; 92 out (text_encode ss); 93 out "</SPAN>") 95 out ("<em>" ^ text_encode ss ^ "</em>") 97 (out "<SPAN class = \"BRKT\">"; 98 out (bracket_trans ss); 99 out "</SPAN>") 101 (out "<DI [all...] |
H A D | Htmlsigs.sml | 5 fun indexbar out srcpath = out (String.concat 153 fun out s = TextIO.output(os, s) function 165 (out "<a name=\""; out target; out "\">"; out anchor; out "</a>") 168 (out "<a href=\"#"; out lin 353 fun out s = TextIO.output(os, s) function [all...] |
H A D | Printbase.sml | 12 fun out s = TextIO.output(os, s) function 31 out (prtseq (prentry, ", ") entries); 32 out "\n"; 40 fun out s = TextIO.output(os, s) function 50 out "\\\\[2ex]\n\n") 53 fun nextstr last [] = out ")\n" 56 (out ", "; out (tt file); nextstr last erest) 58 (out ")\n"; newitem e1 erest) 63 out "\\ite [all...] |
/seL4-l4v-master/HOL4/examples/dev/ |
H A D | vsynth.sml | 247 fun out s = TextIO.output(outstr,s) function 249 (printer out; 265 (* ``DTYPE c (clk,inp,out)`` --> ``DTYPE c (clk,inp,out)`` *) 266 (* ``?v. DTYPE v (clk,inp,out)`` --> ``DTYPE c (clk,inp,out)`` *) 284 (* Test a term has the form ``CONSTANT c out``, *) 302 (* ``CONSTANT c out`` --> ("c", ``out``) where c is Verilog form of c *) 428 fun DTYPEvInst tm (out [all...] |
/seL4-l4v-master/HOL4/src/ring/src/ |
H A D | selftest.sml | 5 fun ntest (i,out) = 6 convtest ("NUM_NORM_CONV " ^ Parse.term_to_string i, NUM_NORM_CONV, i, out)
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | build | 13 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
|
/seL4-l4v-master/isabelle/src/Doc/ |
H A D | prepare_document | 14 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
|
/seL4-l4v-master/HOL4/examples/machine-code/acl2/ |
H A D | Makefile | 7 cat fact-out.lisp 10 /bin/rm fact.lisp fact-out.* untranslate-file.*
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | build | 13 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
|
/seL4-l4v-master/l4v/isabelle/src/Doc/ |
H A D | prepare_document | 14 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | parity.tex | 33 con un input {\small\verb|in|}, un output {\small\verb|out|} e la 34 specifica che l'$n$-esimo output su {\small\verb|out|} � 96 !t. out t = PARITY t inp 104 {\small\verb|inp|} e {\small\verb|out|} soddisfano\footnote{Preferiremmo 110 out(0) = T 118 !t. out(t+1) = (if inp(t+1) then ~(out t) else out t) 127 !inp out. 128 (out [all...] |
/seL4-l4v-master/l4v/misc/filemerge/faster/ |
H A D | translate.cpp | 27 static int to_ascii(wifstream &in, wofstream &out) { argument 29 assert(out.is_open()); 36 out << c; 38 out << t->second; 45 static int to_unicode(wifstream &in, wofstream &out) { argument 47 assert(out.is_open()); 62 out << buffer; 71 out << t->second; 82 out << buffer;
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | File.C | 88 void putUInt(File& out, uint64 val) argument 93 out.putChar(v); 96 out.putChar(0x80 | (v >> 8)), 97 out.putChar((uchar)v); 99 out.putChar(0xA0 | (v >> 16)), 100 out.putChar((uchar)(v >> 8)), 101 out.putChar((uchar)v); 103 out.putChar((v >> 24) | 0xC0), 104 out.putChar((uchar)(v >> 16)), 105 out [all...] |
/seL4-l4v-master/isabelle/Admin/cronjob/ |
H A D | self_update | 17 } > run/self_update.out
|
/seL4-l4v-master/l4v/isabelle/Admin/cronjob/ |
H A D | self_update | 17 } > run/self_update.out
|
/seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
H A D | getting.tex | 246 {\out [| ?P --> ?Q; ?P |] ==> ?Q} 247 {\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm} 249 {\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q} 250 {\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm} 253 appears in{\out slanted typewriter characters}. \ML's response {\out val 265 {\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm} 267 {\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm} 281 {\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm} 283 {\out va [all...] |
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
H A D | getting.tex | 246 {\out [| ?P --> ?Q; ?P |] ==> ?Q} 247 {\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm} 249 {\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q} 250 {\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm} 253 appears in{\out slanted typewriter characters}. \ML's response {\out val 265 {\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm} 267 {\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm} 281 {\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm} 283 {\out va [all...] |