/seL4-l4v-master/HOL4/examples/lambda/other-models/ |
H A D | raw_syntaxScript.sml | 29 collapse e_1 -->_\beta collapse e_2 35 (Where collapse is written graphically in the paper as the "round 41 The collapse function below has the important property that 43 EQC alpha x y = (collapse x = collapse y) 45 I.e., two raw syntax terms are alpha-equivalent iff they collapse 148 (collapse (var s) = VAR s) /\ 149 (collapse (app t u) = collapse [all...] |
/seL4-l4v-master/HOL4/examples/unification/triangular/first-order/ |
H A D | collapseScript.sml | 4 val _ = new_theory "collapse"; 13 collapse s = FUN_FMAP (\v.walkstar s (Var v)) (FDOM s)`; 17 `wfs s ==> !t.(collapse s ��� t = walkstar s t)`, 27 `wfs s ==> !v.v IN FDOM s ==> (collapse s ' v = walkstar s (Var v))`, 41 `wfs s ==> idempotent (collapse s)`, 46 `idempotent s ��� noids s ==> (collapse s = s)`, 49 `FDOM s = FDOM (collapse s)` by SRW_TAC [][collapse_def,FUN_FMAP_DEF] THEN 56 Cases_on `v IN FDOM (collapse s)` THEN SRW_TAC [][] THEN 76 Q_TAC SUFF_TAC `s = collapse s` 78 `FDOM s = FDOM (collapse [all...] |
H A D | substScript.sml | 717 Q.EXISTS_TAC `collapse s` >> 756 `wfs s ==> wfs (collapse s)`, 759 Q_TAC SUFF_TAC `!v u.(vR (collapse s))^+ v u ==> v <> u` 763 Cases_on `u IN FDOM (collapse s)` >> 804 !t.((collapse sx) ��� t = (ss oo s) ��� t)`,
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | FullUnify.sig | 23 val collapse : ((hol_type,hol_type)subst * (term,term) subst) Env.EM value
|
H A D | PmatchHeuristics.sig | 10 collapse_cases : bool, (* collapse cases that lead to same result ? *)
|
H A D | FullUnify.sml | 176 fun collapse E = SOME(E, collapse0 E) function
|
H A D | resolve_then.sml | 135 FullUnify.collapse)
|
/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/ |
H A D | Console.java | 39 gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
|
H A D | TreeNode.java | 84 if (unfold) collapse(); 91 public void collapse() method in class:TreeNode 96 ((Tree)leaves.elementAt(i)).collapse();
|
H A D | GraphView.java | 190 if (!v2.isEmpty()) gra.collapse(v2,"[. . . .]",v1); 199 gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
|
H A D | Graph.java | 943 /* collapse vertices */ 946 public void collapse(Vector vs,String name,Vector inflate) { method in class:Graph
|
/seL4-l4v-master/l4v/isabelle/lib/browser/GraphBrowser/ |
H A D | Console.java | 39 gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
|
H A D | TreeNode.java | 84 if (unfold) collapse(); 91 public void collapse() method in class:TreeNode 96 ((Tree)leaves.elementAt(i)).collapse();
|
H A D | GraphView.java | 190 if (!v2.isEmpty()) gra.collapse(v2,"[. . . .]",v1); 199 gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
|
H A D | Graph.java | 943 /* collapse vertices */ 946 public void collapse(Vector vs,String name,Vector inflate) { method in class:Graph
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | OS.sml | 529 fun collapse [] = [] function 530 | collapse (a :: b) = 534 then collapse b 537 case collapse b of 544 val collapsed = collapse arcs
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sml | 299 fun collapse l = (fst (hd l), List.map snd l); function 301 fun groupsByFst l = List.map collapse (groupsBy fstEq l);
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sml | 299 fun collapse l = (fst (hd l), List.map snd l); function 301 fun groupsByFst l = List.map collapse (groupsBy fstEq l);
|
/seL4-l4v-master/HOL4/src/transfer/ |
H A D | transferLib.sml | 223 case Env.fromEmpty (unify ctys [] (cr_t, h) >> collapse) of 331 collapse)
|
/seL4-l4v-master/HOL4/src/unwind/ |
H A D | unwindLib.sml | 528 (* Could use an itlist here again and collapse the maps. *)
|
/seL4-l4v-master/HOL4/src/pattern_matches/ |
H A D | patternMatchesLib.sml | 346 (* try to collapse rows by introducing a catchall at end*) 364 (* really collapse *) 372 (* could we collapse 2 cases? *)
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | cearTools.sml | 527 (* FIXME: amba_ahb example spends a lot of time here (ctl_grant_always). is ap collapse not working? *)
|
/seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
H A D | advanced.tex | 695 collapse $nat$ to a trivial type:
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
H A D | advanced.tex | 695 collapse $nat$ to a trivial type:
|
/seL4-l4v-master/HOL4/examples/algebra/lib/ |
H A D | GaussScript.sml | 1192 = {{1}, {1}, {1, 2}, {1, 5}} <-- will collapse
|