/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/ |
H A D | heap_wrap.c | 16 struct thing { struct 19 struct thing *left; 20 struct thing *right; 28 void f1(struct thing *t) { 32 void f2(struct thing *t) { 36 void f3(struct thing *t) { 40 void f4(struct thing *t) { 44 void f5(struct thing *p, struct thing t) { 57 int f8(struct list *l, struct thing * [all...] |
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | ptr_modifies.c | 39 struct thing { struct 43 typedef struct thing thing_t;
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibTerm.sig | 127 datatype thing = mlibTerm of term | Formula of formula; type 138 val parse_term' : infixities -> thing quotation -> term 139 val parse_formula' : infixities -> thing quotation -> formula 142 val parse_term : thing quotation -> term 143 val parse_formula : thing quotation -> formula
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | envScript.sml | 34 environments to evaluate to the same thing, rather than not evaluate at all. Using {} is not as satisfactory theoretically but more
|
/seL4-l4v-10.1.1/isabelle/src/HOL/TPTP/TPTP_Parser/ |
H A D | tptp.yacc | 22 | thing => raise (UNRECOGNISED_ROLE thing) 638 | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing) 662 | thing => raise UNRECOGNISED_SYMBOL ("defined_prop", thing) 676 | thing => raise UNRECOGNISED_SYMBOL ("defined_pred", thing) 767 | thing => raise UNRECOGNISED_SYMBOL ("defined_functor", thing) [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ |
H A D | tptp.yacc | 22 | thing => raise (UNRECOGNISED_ROLE thing) 638 | thing => raise UNRECOGNISED_SYMBOL ("defined_type", thing) 662 | thing => raise UNRECOGNISED_SYMBOL ("defined_prop", thing) 676 | thing => raise UNRECOGNISED_SYMBOL ("defined_pred", thing) 767 | thing => raise UNRECOGNISED_SYMBOL ("defined_functor", thing) [all...] |
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/ |
H A D | summary.tex | 32 % define \@xboxverb<thing>\ENDTHEOREM to mean <thing>\ENDTHEOREM 41 % \bboxverb<thing> = <thing> in a verbatim box 5mm from left margin
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | match_goal.sig | 59 Iterate over list, taking first thing that works.
|
H A D | match_goal.sml | 29 thing that raw_match uses. But we are not doing that. *)
|
/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | buildutils.sig | 79 whatever), taking the path to the thing to run, and the
|
/seL4-l4v-10.1.1/HOL4/tools-poly/Holmake/ |
H A D | winNT-systeml.sml | 4 It is the very first thing compiled by the HOL build process so it
|
H A D | unix-systeml.sml | 4 very first thing compiled by the HOL build process so it absolutely
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Functions/document/ |
H A D | intro.tex | 7 sometimes be a difficult thing.
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Functions/document/ |
H A D | intro.tex | 7 sometimes be a difficult thing.
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Hol_pp.sml | 100 fun colour thing col = 101 String.concat["<font color=\"",col,"\">",thing,"</font>"];
|
H A D | Absyn.sml | 122 | dest_typed t = raise ERRloc "dest_typed" (locn_of_absyn t) "Expected a typed thing";
|
/seL4-l4v-10.1.1/HOL4/examples/computability/lambda/ |
H A D | HaltingProblemsScript.sml | 24 if you apply an f to its index, then the thing is undecidable. In
|
/seL4-l4v-10.1.1/HOL4/src/pfl/examples/ |
H A D | tree.sml | 157 Q.PAT_ASSUM `IS_SOME thing` MP_TAC THEN
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | Theory.sig | 123 the last thing done when they load. This will in turn cause a
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | unix-systeml.sml | 4 very first thing compiled by the HOL build process so it absolutely
|
H A D | winNT-systeml.sml | 4 It is the very first thing compiled by the HOL build process so it
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Traverse.sml | 168 (* This code is used just once, to do the right thing with the 193 (* And another thing. The current simplifer doesn't allow users to
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | EnumType.sml | 482 ("thing", ["a0", "a1", "a2", "a3", "a4", "a5", "a6", "a7", "a8", 500 ("thing", ["z0", "z1", "z2", "z3", "z4", "z5", "z6", "z7", "z8", 522 ("thing", ["Z0", "Z1", "Z2", "Z3", "Z4", "Z5", "Z6", "Z7", "Z8",
|
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/ |
H A D | Type.sml | 210 | tymatch any other thing = MERR "different constructors"
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | intSimps.sml | 115 complicated non-presburger thing that will get treated as a variable
|