/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Atom.sig | 10 (* A type for storing first order logic atoms. *)
|
H A D | Units.sml | 63 first check (LiteralNet.match net lit)
|
/seL4-l4v-master/HOL4/polyml/ |
H A D | exportPoly.sml | 51 N.B. polyImport takes the first argument that is not recognised as
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | stack_introLib.sml | 15 val x = first (can (match_term pat)) ps
|
/seL4-l4v-master/HOL4/examples/parity/ |
H A D | PARITY_exercisesScript.sml | 37 (* Specification first:
|
/seL4-l4v-master/isabelle/src/HOL/Hahn_Banach/document/ |
H A D | root.tex | 43 \medskip The document is structured as follows. The first part contains
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Atom.sig | 10 (* A type for storing first order logic atoms. *)
|
H A D | Units.sml | 63 first check (LiteralNet.match net lit)
|
/seL4-l4v-master/l4v/isabelle/src/HOL/Hahn_Banach/document/ |
H A D | root.tex | 43 \medskip The document is structured as follows. The first part contains
|
/seL4-l4v-master/HOL4/src/tfl/src/ |
H A D | Defn.sig | 65 first theorem should be the equations and the second the induction
|
/seL4-l4v-master/HOL4/src/real/ |
H A D | realSimps.sig | 47 common factor must be the first universally quantified variable in
|
/seL4-l4v-master/l4v/isabelle/src/HOL/Data_Structures/document/ |
H A D | root.tex | 74 They were invented by Crane \cite{Crane72}. A first functional implementation
|
/seL4-l4v-master/isabelle/src/HOL/Data_Structures/document/ |
H A D | root.tex | 74 They were invented by Crane \cite{Crane72}. A first functional implementation
|
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | ThyDataSexp.sig | 74 val first : 'a dec list -> 'a dec value
|
/seL4-l4v-master/HOL4/Manual/LaTeX/ |
H A D | ack.tex | 42 added material on first order proof search; and Tjark Weber, who wrote 52 and improvement, the \HOL\ logic is unchanged since the first edition 94 sending lists of errors in the first edition. Thanks to everyone who
|
/seL4-l4v-master/HOL4/src/bag/ |
H A D | bagSimpleLib.sml | 54 (*add first element again*) 57 (*swap the first two elements*) 70 (*first bring the first element, i.e. n, to the front*) 73 (*remove first element*)
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Cache.sml | 34 fun first p [] = raise FIRST function 35 | first p (h::t) = if p h then h else first p t 48 (case snd (first ok prevs) of 347 in this situation should first try conv on the original
|
/seL4-l4v-master/HOL4/tools/mlyacc/src/ |
H A D | mklrtable.sml | 137 (* method for filling tables - first compute the reductions called for in a 143 for reduction by that item. The first reduction is mapped to a list of 309 val {nullable,first} = 317 first=first,
|
/seL4-l4v-master/HOL4/polyml/modules/ |
H A D | Makefile.in | 168 first=`echo "$$dir1" | sed -e "$$sed_first"`; \ 169 if test "$$first" != "."; then \ 170 if test "$$first" = ".."; then \ 175 if test "$$first2" = "$$first"; then \ 180 dir0="$$dir0"/"$$first"; \
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | bootup.tex | 28 first slot of the CNode has CPTR 0x0, the second slot has CPTR 0x1 etc. 30 The first 12 slots contain specific capabilities as listed in 87 \texttt{end} being the CPTR of the first slot after the region ends, i.e.\ 146 ordered such that the first capability references the first frame of the
|
/seL4-l4v-master/HOL4/src/pred_set/src/more_theories/ |
H A D | ordinalNotationScript.sml | 438 (* The set of all first exponents of ordinals anywhere in S is n.e. and *) 462 (* element that alpha_1 is the first exponent of. There may be more than one *) 472 (* Now consider the subset of sj where all the ordinals have first exponent *) 484 (* Now we want to consider the set of all first coeff. for any ordinal in *) 506 (* Consider the subset of ordinals in s_alpha_1 that have k_1 as first expt. *) 544 (* Start first case. There is a "d" in Tails with rank <=n. *) 593 (* End first case. *)
|
/seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
H A D | getting.tex | 23 and demonstrates forward proof. The examples are set in first-order logic. 24 The command to start Isabelle running first-order logic is 172 To illustrate the notation, consider two axioms for first-order logic: 225 resolves the conclusion of $thm1$ with the first premise of~$thm2$. 237 first-order logic.\footnote{For a listing of the FOL rules and their \ML{} 242 first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with 412 first premise by assumption. But \texttt{eresolve_tac} additionally deletes 470 first-order logic. Let us try the example from \S\ref{prop-proof}, 502 deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using 700 first [all...] |
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
H A D | getting.tex | 23 and demonstrates forward proof. The examples are set in first-order logic. 24 The command to start Isabelle running first-order logic is 172 To illustrate the notation, consider two axioms for first-order logic: 225 resolves the conclusion of $thm1$ with the first premise of~$thm2$. 237 first-order logic.\footnote{For a listing of the FOL rules and their \ML{} 242 first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with 412 first premise by assumption. But \texttt{eresolve_tac} additionally deletes 470 first-order logic. Let us try the example from \S\ref{prop-proof}, 502 deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using 700 first [all...] |
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibClause.sml | 432 fun neq_simp1 cl = first (total (dest_neq cl)) (literals cl); 526 necessary) to make the first hit an Id. 531 clause. If M was the largest, then keep the first hit an Id. If N was 532 the largest, then make the first hit a Sym. If in the previous step we 533 had to flip all the hits to make the first hit an Id, then flip this 534 first hit too.
|
/seL4-l4v-master/HOL4/examples/finite-test-set/ |
H A D | finite_test_setScript.sml | 7 UOK Every first-order formula (in prenex normal form) over the natural numbers is 20 UOK Thus, every first-order formula can be decided by checking a single instance. 21 UOK This sounds surprising at first, until you realise what is not shown: how to
|