Searched refs:nl (Results 1 - 25 of 58) sorted by relevance

123

/seL4-l4v-10.1.1/HOL4/examples/computability/
H A DgoedelCodeScript.sml193 (`!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 DHexSolitaireScript.sml190 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 DSolitaireScript.sml233 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 DgfgScript.sml51 ���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 DKatiPuzzleScript.sml207 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 Dgr_t.sml219 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 Dgr_t.sml219 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 Dgr_t.sml219 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 Ddepcomp110 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 Dinstall-sh45 nl='
47 IFS=" $tab$nl"
131 *' '* | *"$tab"* | *"$nl"* | *'*'* | *'?'* | *'['*)
H A Dcompile31 nl='
36 IFS=" "" $nl"
/seL4-l4v-10.1.1/HOL4/polyml/
H A Ddepcomp110 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 Dinstall-sh45 nl='
47 IFS=" $tab$nl"
131 *' '* | *"$tab"* | *"$nl"* | *'*'* | *'?'* | *'['*)
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Dpretty.scala89 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 Dpretty.scala89 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 DSerpent_Bitslice_KeyScheduleScript.sml22 = 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 DDep.sml44 let fun distrib (s,nl) = map (fn n => (s,n)) nl in
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DTheoryReader.sml113 "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 Ddocument_structure.scala184 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 Dmlpp34 my $nl = chomp $quote;
51 if (0 < $nl) {
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Isar/
H A Ddocument_structure.scala184 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 Dmlpp34 my $nl = chomp $quote;
51 if (0 < $nl) {
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DmuSyntax.sml485 | "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 DminisatResolve.sml99 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 DtttTermData.sml129 "TYOP" :: nl => TYOP (map string_to_int nl)

Completed in 205 milliseconds

123