Searched refs:unfold (Results 1 - 18 of 18) sorted by relevance

/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/
H A DTreeNode.java22 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 DTreeNode.java22 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 Dunary_recfnsScript.sml86 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 DtttUnfold.sml804 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 DpathScript.sml1375 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 DltreeScript.sml347 (* ltree unfold *)
/seL4-l4v-master/HOL4/examples/fun-op-sem/small-step/
H A Dpath_auxScript.sml303 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 DchurchlistScript.sml504 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 DFOL.tex467 \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 DZF.tex1690 \isa{unfold list.con_defs [symmetric]}.
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics_ZF/document/
H A DFOL.tex467 \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 DZF.tex1690 \isa{unfold list.con_defs [symmetric]}.
/seL4-l4v-master/HOL4/src/unwind/Manual/
H A Ddescription.tex135 The function \ml{EXPAND\_AUTO\_RIGHT\_RULE} can be used to unfold, unwind and
/seL4-l4v-master/isabelle/src/Doc/Intro/document/
H A Dadvanced.tex148 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 Dadvanced.tex148 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 Ddescription.tex348 \noindent Here, we have used \ml{string\_CONV} to iteratively unfold the formal
/seL4-l4v-master/l4v/misc/vim/
H A Disabelle.vim196 syn keyword IsabelleCommandMethod fold unfold unfold_locales unfolding
/seL4-l4v-master/HOL4/examples/algebra/lib/
H A DtriangleScript.sml564 = lcm (1 4 6 4 1) --> unfold 5x to add 5 times

Completed in 312 milliseconds