Searched refs:unfold (Results 1 - 18 of 18) sorted by relevance
/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/ |
H A D | TreeNode.java | 22 boolean unfold=false; field in class:TreeNode 27 unfold=unfold||u; 29 unfold=unfold||u; 63 unfold=u; 72 if (unfold) 84 if (unfold) collapse(); 85 else unfold=true; 93 unfold [all...] |
/seL4-l4v-master/l4v/isabelle/lib/browser/GraphBrowser/ |
H A D | TreeNode.java | 22 boolean unfold=false; field in class:TreeNode 27 unfold=unfold||u; 29 unfold=unfold||u; 63 unfold=u; 72 if (unfold) 84 if (unfold) collapse(); 85 else unfold=true; 93 unfold [all...] |
/seL4-l4v-master/HOL4/examples/computability/ |
H A D | unary_recfnsScript.sml | 86 unfold 0 m = [] ��� 87 unfold (SUC n) m = if n = 0 then [m] 88 else nfst m :: unfold n (nsnd m) 92 unfold 1 n = [n] 98 ���m n. LENGTH (unfold m n) = m 104 unfold a n = [] ��� a = 0 116 ���a n. 0 < a ��� fold (unfold a n) = n 119 Cases_on ���unfold a (nsnd n)��� >> fs[] >> 124 ���l. unfold (LENGTH l) (fold l) = l 130 n = LENGTH l ��� unfold [all...] |
/seL4-l4v-master/HOL4/src/tactictoe/src/ |
H A D | tttUnfold.sml | 804 fun unfold in_flag stack program = case program of function 813 val new_body = unfold 0 lstack body 828 unfold in_flag (push_stackvl in_flag stackvl stack) m 833 Open sl :: unfold in_flag (push_stackvl in_flag stackvl stack) m 836 (infix_glob := vl @ (!infix_glob); Infix vl :: unfold in_flag stack m) 837 | In :: m => In :: unfold (in_flag + 1) stack m 839 Start s :: unfold in_flag (dempty String.compare :: stack) m 840 | End :: m => End :: unfold (in_flag - 1) (tl stack) m 849 Code ("op",Protect) :: new_code :: unfold in_flag stack m 864 new_code :: unfold in_fla [all...] |
/seL4-l4v-master/HOL4/src/coalgebras/ |
H A D | pathScript.sml | 1375 Define `unfold proj f s = 1386 unfold proj f s = 1389 | SOME (s',l) => pcons (proj s) l (unfold proj f s')`, 1399 ((f x = NONE) ==> (unfold proj f x = stopped_at (proj x))) /\ 1401 (unfold proj f x = pcons (proj x) v2 (unfold proj f v1)))`, 1408 `!proj f s. labels (unfold proj f s) = LUNFOLD f s`, 1434 okpath m (unfold proj f s)`, 1438 Q.EXISTS_TAC `\p. ?s. P s /\ (p = unfold proj f s)` THEN 1484 Q.EXISTS_TAC `unfold (��( [all...] |
H A D | ltreeScript.sml | 347 (* ltree unfold *)
|
/seL4-l4v-master/HOL4/examples/fun-op-sem/small-step/ |
H A D | path_auxScript.sml | 303 unfold (\(p1,p2). (first p1, first p2)) 494 qexists_tac `unfold (\s. s) (\s. some (s',l). r s l s') s` >>
|
/seL4-l4v-master/HOL4/examples/computability/lambda/ |
H A D | churchlistScript.sml | 504 fold and unfold 634 ���n m. cunfold @@ church n @@ church m == cvlist (MAP church (unfold n m))
|
/seL4-l4v-master/isabelle/src/Doc/Logics_ZF/document/ |
H A D | FOL.tex | 467 \isa{unfold} method, which expands 474 \isacommand{apply}\ (unfold\ not\_def)\isanewline 783 This time, we simply unfold using the definition of $if$:
|
H A D | ZF.tex | 1690 \isa{unfold list.con_defs [symmetric]}.
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics_ZF/document/ |
H A D | FOL.tex | 467 \isa{unfold} method, which expands 474 \isacommand{apply}\ (unfold\ not\_def)\isanewline 783 This time, we simply unfold using the definition of $if$:
|
H A D | ZF.tex | 1690 \isa{unfold list.con_defs [symmetric]}.
|
/seL4-l4v-master/HOL4/src/unwind/Manual/ |
H A D | description.tex | 135 The function \ml{EXPAND\_AUTO\_RIGHT\_RULE} can be used to unfold, unwind and
|
/seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
H A D | advanced.tex | 148 Taking this point of view, Isabelle does not unfold definitions 225 above, with an additional step to unfold negation in the major premise.
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
H A D | advanced.tex | 148 Taking this point of view, Isabelle does not unfold definitions 225 above, with an additional step to unfold negation in the major premise.
|
/seL4-l4v-master/HOL4/src/string/Manual/ |
H A D | description.tex | 348 \noindent Here, we have used \ml{string\_CONV} to iteratively unfold the formal
|
/seL4-l4v-master/l4v/misc/vim/ |
H A D | isabelle.vim | 196 syn keyword IsabelleCommandMethod fold unfold unfold_locales unfolding
|
/seL4-l4v-master/HOL4/examples/algebra/lib/ |
H A D | triangleScript.sml | 564 = lcm (1 4 6 4 1) --> unfold 5x to add 5 times
|
Completed in 303 milliseconds