| /seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
| H A D | MutRecMask.sml | 2 * Provides a way to allow constructor names to be rebound.
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | UGeneral.sml | 12 infix 5 to
13 fun n to m = if n > m then [] else n::(n+1 to m)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | UGeneral.sml | 12 infix 5 to
13 fun n to m = if n > m then [] else n::(n+1 to m)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
| H A D | UGeneral.sml | 12 infix 5 to
13 fun n to m = if n > m then [] else n::(n+1 to m)
|
| /seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/official-semantics/ |
| H A D | ClockedSemanticsScript.sml | 44 * Set default parsing to natural numbers rather than integers
53 * A simpset fragment to rewrite away quantifiers restricted with :: (a to b)
75 (!i :: (0 to (LENGTH w - 1)). B_SEM (ELEM w i) (B_NOT c))
96 ?i :: (0 to LENGTH w).
103 * (see commented out stuff) to avoid need for TFL hacks to prove termination.
116 ?i :: (1 to LENGTH w).
122 ?k :: (0 to LENGTH w).
126 !j :: (0 to
[all...] |
| H A D | UnclockedSemanticsScript.sml | 42 * Set default parsing to natural numbers rather than integers
56 * pureDefine doesn't export definitions to theCompset (for EVAL).
133 ?k :: (0 to LENGTH w).
134 OLD_UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). OLD_UF_SEM (RESTN w j) f1)
137 !j :: (0 to LENGTH w).
141 !j :: (0 to LENGTH w).
144 ?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
147 !j :: (0 to LENGTH w).
150 ((?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
152 (!k :: (j to LENGT
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/ |
| H A D | tempScript.sml | 4 * A template theory script suitable for Holmake. If you are going to use it *
5 * for theory "x", you must change the name of this file to "xScript.sml", *
6 * and the argument to "new_theory" below must be changed to be "x". *
18 * Next, bring in extra tools used. For example, if you were going to use *
19 * bossLib, then while you were working interactively, you may have to *
28 * However, when using the batch compiler, the call to "load" isn't allowed. *
31 * refer to modules that are used. *
48 * Write the theory to disk. *
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Ho_Net.sig | 3 * MODIFIED : Donald Syme, 1995, to add local constants
5 * MODIFIED : Donald Syme, November 1995, to be keyed up to
|
| H A D | fastbuild.sml | 2 (* This structure is used by Holmake to provide a "fast" mode of running *)
4 (* (and store_thm) function to be a call to mk_thm, so proofs that require *)
6 (* still has to be evaluated before it is then discarded. But use of this *)
|
| /seL4-l4v-10.1.1/HOL4/src/simp/src/ |
| H A D | Cache.sig | 9 term is relevant to the decision procedure i.e., might be
11 term t to |- t = x for some value x.
13 Returns a new conversion, and a reference to a table used as a
14 cache. The table is returned to enable users to analyse its
18 functions where it is inappropriate to have hypotheses that don't
20 is to be shown equal to some other value. The extra, first,
21 parameter to RCACHE is a function that when applied to
[all...] |
| H A D | congLib.sig | 2 (* Simplification of terms similar to SIMP_CONV but regarding arbitrary *)
15 * it is limited to simplify a term t1 to a term t2 which is equivalent
16 * according to the congruence =. The underlying traverser (TRAVERSER.sml)
17 * however is able to handle arbitrary congruences.
19 * This lib tries to provide this ability of the traverser to handle arbitrary
20 * congruences (or in fact preorders) to the end user. Therefore, an
21 * interface similar to the interface of SimpLib is provided.
28 * Similar to ssfra
[all...] |
| H A D | Traverse.sig | 19 type context = exn (* well known SML hack to allow any kind of data *)
23 * These are the things that get applied to terms during
25 * current term reduces to a related
28 * of the forms above - Nb. in SML exceptions are able to contain
30 * is a hack, but it is the best way to get good data hiding in SML
31 * without resorting to functors)
36 * the traversal engine to the reduce routine are:
38 * A continuation function, to be used if the reducer needs to
39 * solve some side conditions and want to continu
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibTermorder.sml | 182 (* A partial order on equations, designed to be quick to check. *)
212 (* only if the termorder is known to be satisfiable. *)
256 fun chatto n s (to as TO (_,vars,eqns,_)) =
258 (chat (s ^ ":\n" ^ termorder_to_string to ^ "\n");
277 fun add_leq lr (to as TO (parm,vars,eqns,_)) =
287 val () = chatto 1 "add_leq input" to
290 val to = TO (parm,vars',eqns',false) value
291 val () = chatto 1 "add_leq result" to
293 to
360 val to = TON parm eqns' value
385 val to = value
[all...] |
| /seL4-l4v-10.1.1/HOL4/tools-poly/poly/ |
| H A D | Binarymap.sig | 6 (* Original implementation due to Stephen Adams, Southampton, UK *)
30 'key to range type 'a, or equivalently, applicative dictionaries
37 [insert(m, i, v)] extends (or modifies) map m to map i to v.
39 [find (m, k)] returns v if m maps k to v; otherwise raises NotFound.
41 [peek(m, k)] returns SOME v if m maps k to v; otherwise returns NONE.
44 modified map and the element v corresponding to k. Raises NotFound
53 [app f m] applies function f to the entries (k, v) in m, in
54 increasing order of k (according to the ordering ordr used to
[all...] |
| H A D | Help.sig | 34 t move to top of file
35 b move to bottom of file
42 [helpdirs] is a reference to a list of additional directories to be
46 [indexfiles] is a reference to a list of full paths of help term
50 [specialfiles] is a reference to a list of {term, file, title}
51 records, each of which maps a search term to the specified file
53 `term' field should be all lowercase, since the argument passed to
54 `help' will be converted to lowercase.
56 [welcome] is a reference to th
[all...] |
| /seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
| H A D | protocol.tex | 11 Communications security is an ancient art. Julius Caesar is said to have
21 messages. People who wish to communicate securely over such a network can
22 use cryptography, but if they are to understand each other, they need to
29 format, fooling an honest party. The adversary might be able to masquerade
34 reply must include a copy of that nonce, to prove that it is not a replay of
37 different one. You should be starting to see that protocol design is
43 Proposed in 1978, it was found to be defective nearly two decades
45 how to verify protocols using Isabelle.
51 This protocol uses public-key cryptography. Each person has a private key, known only to
[all...] |
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
| H A D | protocol.tex | 11 Communications security is an ancient art. Julius Caesar is said to have
21 messages. People who wish to communicate securely over such a network can
22 use cryptography, but if they are to understand each other, they need to
29 format, fooling an honest party. The adversary might be able to masquerade
34 reply must include a copy of that nonce, to prove that it is not a replay of
37 different one. You should be starting to see that protocol design is
43 Proposed in 1978, it was found to be defective nearly two decades
45 how to verify protocols using Isabelle.
51 This protocol uses public-key cryptography. Each person has a private key, known only to
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | parse_type.sig | 27 (* The record of functions specify how to deal with the need to
31 should be accepted as suffixes. With this set to true, the parser
35 The parameter is set to true for parsing datatype definitions, where
36 it is useful to be able to mention types that don't actually exist
|
| /seL4-l4v-10.1.1/isabelle/src/HOL/TPTP/TPTP_Parser/ |
| H A D | tptp.lex | 5 * Omit %full in definitions to restrict alphabet to ascii.
6 * Could include %posarg to ensure that we'd start counting character positions
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ |
| H A D | tptp.lex | 5 * Omit %full in definitions to restrict alphabet to ascii.
6 * Could include %posarg to ensure that we'd start counting character positions
|
| /seL4-l4v-10.1.1/seL4/manual/parts/ |
| H A D | intro.tex | 4 % This software may be distributed and modified according to the terms of
15 The seL4 microkernel is an operating-system kernel designed to be
18 services to applications, such as abstractions to create and manage virtual address
20 of services provided by seL4 directly translates to a small
22 the ARMv6 version of the kernel to be formally proven in the Isabelle/HOL
23 theorem prover to adhere to its formal
34 seL4 kernel to userspace.
36 While we have tried to ensur
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/Boolify/src/ |
| H A D | Encode.sig | 4 (* Basically the same as Konrad Slind's code to generate size functions *)
|
| /seL4-l4v-10.1.1/HOL4/src/marker/ |
| H A D | markerLib.sig | 67 from left to right.
72 from left to right.
74 [move_stmarked_conj_left t] moves the st-marked conjunct in t to
81 [move_stmarked_conj_right t] moves the st-marked conjunct to the
82 right. Analogous to move_stmarked_conj_left.
84 [move_stmarked_disj_left t] moves the st-marked disjunct to the
85 left. Analogous to move_stmarked_conj_left.
87 [move_stmarked_disj_right t] moves the st-marked disjunct to the
88 right. Analogous to move_stmarked_conj_left.
91 and then moves it to th
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/executable-semantics/ |
| H A D | test2.v | 13 // Can't assign to output wires, so need to connect them to registers
31 @(posedge BtoS_ACK) // Wait for ack to be asserted
35 @(negedge BtoS_ACK) // Wait for ack to be de-asserted
37 DI_reg = DI_reg + 1; // Increment data to be sent next iteration
46 // Receive data from Sender and then send it to Receiver
58 // Can't assign to output wires, so need to connect them to register
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsLibSimple.sig | 12 to Unwind. It allows more syntax than Unwind and can be
34 - avoid : a set of variables to avoid in the instantiation
36 - v : variable to search an instance for
37 - tm : a term to search an instantiation in
49 Having an additional callback argument to search guesses for subterms is also useful.
70 (* to find guesses for equations, a function can also be applied to
71 both sides of the equation first. For example, to find guesses
72 for "x" in "(x, y) = f z" it might be useful to apply "FST" to
[all...] |