/seL4-l4v-10.1.1/HOL4/examples/computability/ |
H A D | goedelCodeScript.sml | 193 (`!gn i nl. (gn = GCODE i nl) ==> (GDECODE i gn = SOME nl)`, 198 `?h t. nl = h::t` by METIS_TAC [listTheory.list_CASES,GCODE_EQ_1] THEN 215 `!nl i. GDECODE i (GCODE i nl) = SOME nl`, 222 `!nl. DECODE (ENCODE nl) = nl`, [all...] |
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/ |
H A D | HexSolitaireScript.sml | 190 fun nl () = print"\n" function 192 (print" ";p 1 ;sp();p 2 ;sp();p 3 ;nl(); 193 print" " ;p 4 ;sp();p 5 ;sp();p 6 ;sp();p 7 ;nl(); 194 print" " ;p 8 ;sp();p 9 ;sp();p 10;sp();p 11;sp();p 12;nl(); 195 print" " ;p 13;sp();p 14;sp();p 15;sp();p 16;nl(); 196 print" ";p 17;sp();p 18;sp();p 19;nl();nl())
|
H A D | SolitaireScript.sml | 233 fun nl () = print"\n" function 235 (print" ";p 07;p 14;p 21;nl(); 236 print" ";p 08;p 15;p 22;nl(); 237 p 01;p 04;p 09;p 16;p 23;p 28;p 31;nl(); 238 p 02;p 05;p 10;p 17;p 24;p 29;p 32;nl(); 239 p 03;p 06;p 11;p 18;p 25;p 30;p 33;nl(); 240 print" ";p 12;p 19;p 26;nl(); 241 print" ";p 13;p 20;p 22;nl();nl())
|
/seL4-l4v-10.1.1/HOL4/examples/generic_finite_graphs/ |
H A D | gfgScript.sml | 51 ���k nl e n. lookup k adjmap = SOME nl ��� MEM (e,n) nl ��� 86 >- (rename[`lookup k _ = SOME nl`, `MEM (e',n) nl`]
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/KatiPuzzle/ |
H A D | KatiPuzzleScript.sml | 207 fun nl () = print"\n" function 211 (nl(); 212 (if flag then (print" "; pb(s 12, s 11, s 10, s 9) ; nl()) else ()); 213 print" " ;p 0 ;sp();p 1 ;sp();p 2 ;nl(); 214 print" | | |"; nl(); 215 print" " ;p 3 ;sp();p 4 ;sp();p 5 ;nl(); 216 print" | | |"; nl(); 217 print" " ;p 6 ;sp();p 7 ;sp();p 8 ;nl(); nl(); nl()) [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | gr_t.sml | 219 fun mkgr (nl,el) = 229 (insEdges (insNodes (M.empty,0,nl),el),length nl-1) 295 fun mkgr (nl,el) = 305 (insEdges (insNodes (M.empty,0,nl),el),length nl-1) 339 fun mkgr (nl,el) = 346 (insEdges (insNodes (M.empty,0,nl),el),length nl-1) 378 fun mkgr (nl,e [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | gr_t.sml | 219 fun mkgr (nl,el) = 229 (insEdges (insNodes (M.empty,0,nl),el),length nl-1) 295 fun mkgr (nl,el) = 305 (insEdges (insNodes (M.empty,0,nl),el),length nl-1) 339 fun mkgr (nl,el) = 346 (insEdges (insNodes (M.empty,0,nl),el),length nl-1) 378 fun mkgr (nl,e [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | gr_t.sml | 219 fun mkgr (nl,el) = 229 (insEdges (insNodes (M.empty,0,nl),el),length nl-1) 295 fun mkgr (nl,el) = 305 (insEdges (insNodes (M.empty,0,nl),el),length nl-1) 339 fun mkgr (nl,el) = 346 (insEdges (insNodes (M.empty,0,nl),el),length nl-1) 378 fun mkgr (nl,e [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | depcomp | 110 nl=' 241 tr ' ' "$nl" < "$tmpdepfile" \ 275 tr ' ' "$nl" < "$tmpdepfile" \ 277 | tr "$nl" ' ' >> "$depfile" 280 tr ' ' "$nl" < "$tmpdepfile" \ 612 tr ' ' "$nl" < "$tmpdepfile" \ 670 | tr ' ' "$nl" \
|
H A D | install-sh | 45 nl=' 47 IFS=" $tab$nl" 131 *' '* | *"$tab"* | *"$nl"* | *'*'* | *'?'* | *'['*)
|
H A D | compile | 31 nl=' 36 IFS=" "" $nl"
|
/seL4-l4v-10.1.1/HOL4/polyml/ |
H A D | depcomp | 110 nl=' 241 tr ' ' "$nl" < "$tmpdepfile" \ 275 tr ' ' "$nl" < "$tmpdepfile" \ 277 | tr "$nl" ' ' >> "$depfile" 280 tr ' ' "$nl" < "$tmpdepfile" \ 612 tr ' ' "$nl" < "$tmpdepfile" \ 670 | tr ' ' "$nl" \
|
H A D | install-sh | 45 nl=' 47 IFS=" $tab$nl" 131 *' '* | *"$tab"* | *"$nl"* | *'*'* | *'?'* | *'['*)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | pretty.scala | 89 private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0) 91 def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1) 168 val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | pretty.scala | 89 private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0) 91 def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1) 168 val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/Serpent/Bitslice/ |
H A D | Serpent_Bitslice_KeyScheduleScript.sml | 22 = let nl =((w_1 ?? w_3 ?? w_5 ?? w_8 ?? PHI ?? (n2w:num->word32) (131-i)) #>> 27 then nl 28 else makeSubKeyBitSlice nl (i-1)`,
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | Dep.sml | 44 let fun distrib (s,nl) = map (fn n => (s,n)) nl in
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | TheoryReader.sml | 113 "TYOP" :: nl => TYOP (map string_to_int nl) 171 let val (nl,cont) = wait_nonumber [] (tl l) in value 172 (read_string (hd l), map string_to_int nl) :: read_dl cont
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Isar/ |
H A D | document_structure.scala | 184 val nl = new ML_Item(ML_Lex.Token(ML_Lex.Kind.SPACE, "\n"), None) 209 sections.add(nl)
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/scripts/ |
H A D | mlpp | 34 my $nl = chomp $quote; 51 if (0 < $nl) {
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Isar/ |
H A D | document_structure.scala | 184 val nl = new ML_Item(ML_Lex.Token(ML_Lex.Kind.SPACE, "\n"), None) 209 sections.add(nl)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/scripts/ |
H A D | mlpp | 34 my $nl = chomp $quote; 51 if (0 < $nl) {
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | muSyntax.sml | 485 | "Not" => let val (nf,nl) = uniq (List.hd args) l subs in (``~(^nf)``,nl) end 488 | "DIAMOND" => let val (nf,nl) = uniq (List.last args) l subs in (``<<^(List.hd args)>> (^nf)``,nl) end 489 | "BOX" => let val (nf,nl) = uniq (List.last args) l subs in (``[[^(List.hd args)]] (^nf)``,nl) end 493 val (nf,nl) = uniq (List.last args) (l@[nn]) subs 494 in (``mu ^(nn) .. ^nf``,l@nl) end 495 else let val (nf,nl) = uniq (List.last args) ((List.hd args)::l) subs in (``mu ^(List.hd args) .. ^nf``,l@nl) en [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | minisatResolve.sml | 99 fun resolveChain lfn sva cl (nl,lnl) rci = 100 let val ((_,c0i),(vi,c1i),nlt) = l2hh nl
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttTermData.sml | 129 "TYOP" :: nl => TYOP (map string_to_int nl)
|