/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/ |
H A D | TreeNode.java | 21 Vector leaves=new Vector(10,10); field in class:TreeNode 26 leaves.addElement(new TreeNode(n,p,num)); 38 Enumeration e1=leaves.elements(); 49 leaves.addElement(nd); 73 for (int i=0;i<leaves.size();i++) 75 TreeNode t=((TreeNode)leaves.elementAt(i)).lookup(y); 83 if (!leaves.isEmpty()) { 95 for(int i=0;i<leaves.size();i++) 96 ((Tree)leaves.elementAt(i)).collapse(); 102 Enumeration e1=leaves [all...] |
/seL4-l4v-master/l4v/isabelle/lib/browser/GraphBrowser/ |
H A D | TreeNode.java | 21 Vector leaves=new Vector(10,10); field in class:TreeNode 26 leaves.addElement(new TreeNode(n,p,num)); 38 Enumeration e1=leaves.elements(); 49 leaves.addElement(nd); 73 for (int i=0;i<leaves.size();i++) 75 TreeNode t=((TreeNode)leaves.elementAt(i)).lookup(y); 83 if (!leaves.isEmpty()) { 95 for(int i=0;i<leaves.size();i++) 96 ((Tree)leaves.elementAt(i)).collapse(); 102 Enumeration e1=leaves [all...] |
/seL4-l4v-master/HOL4/src/integer/ |
H A D | OmegaSymbolic.sig | 22 as long as the leaves are relations over integer expressions. 25 leaves are relations over integer expressions), finds a quantifier
|
H A D | OmegaMath.sig | 96 disjunction of two normalised <= leaves. (The latter happens if 115 where body is a conjunction of leaves, possibly including 123 where body is a conjunction of leaves, possibly including
|
H A D | OmegaSymbolic.sml | 42 leaves. 481 Given a list of variables vs, and a conjunction of leaves t, pick the 569 fully normalised leaves. This function picks one of the quantifiers
|
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
H A D | tailrecLib.sml | 76 fun leaves (FUN_VAL tm) f = FUN_VAL (f tm) function 77 | leaves (FUN_COND (c,t)) f = FUN_COND (c, leaves t f) 78 | leaves (FUN_IF (a,b,c)) f = FUN_IF (a, leaves b f, leaves c f) 79 | leaves (FUN_LET (v,y,t)) f = FUN_LET (v, y, leaves t f) 101 fun leaves_inl body f1 f2 = ftree2tm (leaves (tm2ftree body) (fn tm => 145 val pre_tm = ftree2tm (leaves (tm2ftre [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
H A D | reg_allocLib.sml | 214 fun leaves (FUN_COND (_,t)) = leaves t function 215 | leaves (FUN_LET (_,_,t)) = leaves t 216 | leaves (FUN_IF (_,t1,t2)) = leaves t1 @ leaves t2 217 | leaves (FUN_VAL tm) = [tm] 218 val bases = filter (not o can (match_term lhs)) (leaves (tm2ftree rhs)) 278 fun leaves (FUN_CON function [all...] |
/seL4-l4v-master/HOL4/src/boss/ |
H A D | selftest.sml | 193 val _ = tprint "Simp -* APPEND_ASSOC leaves list unchanged" 196 val _ = tprint "Simp -* list.APPEND_ASSOC leaves list unchanged" 200 val _ = tprint "Simp -* list.APPEND_ASSOC.1 leaves list unchanged" 204 val _ = tprint "Simp Excl APPEND_ASSOC leaves list unchanged" 207 val _ = tprint "Simp Excl list.APPEND_ASSOC leaves list unchanged" 213 printarg = fn _ => "simp Excl on arith d.p. leaves input unchanged",
|
/seL4-l4v-master/HOL4/src/real/ |
H A D | selftest.sml | 165 fn _ => "simp w/o nat d.p. but with real d.p. leaves input unchanged", 172 fn _ => "simp with nat d.p. but w/o real d.p. leaves input unchanged",
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | boolSimps.sig | 50 Note that it leaves ==> alone, but includes the following
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | source_valuesScript.sml | 8 leaves are natural numbers (num) *)
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibUseful.sml | 650 fun f (LEAF _) = {leaves = 1, branches = 0} 651 | f (BRANCH (_, ts)) = foldl g {leaves = 0, branches = 1} ts 652 and g (t, {leaves = l, branches = b}) = 653 let val {leaves=l', branches=b'} = f t in {leaves=l+l', branches=b+b'} end;
|
H A D | mlibUseful.sig | 173 val tree_size : ('a,'b) tree -> {branches : int, leaves : int}
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/ |
H A D | binary-trees.ml | 91 % The next one counts the number of leaves in the tree. %
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Preterm.sig | 57 if the types attached to the leaves aren't valid for the kernel. *)
|
H A D | Literal.sml | 6 * difference in treatment between zero and the other numerals leaves
|
/seL4-l4v-master/HOL4/examples/ |
H A D | Thery.sml | 68 This leaves two goals. The first is easy to show.
|
/seL4-l4v-master/HOL4/examples/lambda/typing/ |
H A D | contextlistsScript.sml | 9 (* permutation over contexts swaps the strings and leaves the types alone *)
|
/seL4-l4v-master/HOL4/src/lite/ |
H A D | liteLib.sml | 388 (* Apply at leaves of op-tree; NB any failures at leaves cause failure. *)
|
/seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
H A D | skiTools.sml | 209 fun add a [] leaves = LEAF a :: leaves
|
/seL4-l4v-master/HOL4/examples/machine-code/decompiler/ |
H A D | decompilerLib.sml | 1397 fun leaves (FUN_VAL tm) f = FUN_VAL (f tm) function 1398 | leaves (FUN_COND (c,t)) f = FUN_COND (c, leaves t f) 1399 | leaves (FUN_IF (a,b,c)) f = FUN_IF (a, leaves b f, leaves c f) 1400 | leaves (FUN_LET (v,y,t)) f = FUN_LET (v, y, leaves t f) 1596 free_vars o rm_pc o ftree2tm o leaves t) 1600 free_vars o rm_pc o ftree2tm o leaves [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | patternMatch.sml | 20 (* leaves, executing the tests corresponding to the test nodes along the path. *)
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_astScript.sml | 14 It leaves out the following which don't correspond to a PowerPC instruction:
|
/seL4-l4v-master/HOL4/src/unwind/Manual/ |
H A D | description.tex | 252 Unwinding {\small\verb%l3%} then leaves us with the required recursive 475 the internal lines except for {\small\verb%l4%} can be pruned. This leaves
|
/seL4-l4v-master/HOL4/examples/dev/sw2/test/ |
H A D | tea.sml | 204 (* TEAEncrypt unwound a bit, but leaves some simplifications still possible *)
|