Searched refs:system (Results 1 - 25 of 246) sorted by relevance

12345678910

/seL4-l4v-10.1.1/HOL4/tools/quote-filter/
H A Dselftest.sml3 val _ = system "./quote-filter input temp-output"
5 val result = system "diff temp-output desired-output"
/seL4-l4v-10.1.1/l4v/misc/benchmark/
H A Dspeedstep.sh11 FREQ_AVAIL=/sys/devices/system/cpu/cpu0/cpufreq/scaling_available_frequencies
12 FREQ_CONTROL=/sys/devices/system/cpu/cpu0/cpufreq/scaling_setspeed
13 FREQ_GOV=/sys/devices/system/cpu/cpu0/cpufreq/scaling_governor
14 FREQ_CUR=/sys/devices/system/cpu/cpu0/cpufreq/scaling_cur_freq
/seL4-l4v-10.1.1/seL4/include/model/
H A Dsmp.h25 nodeState_t system; member in struct:smpStatedata
/seL4-l4v-10.1.1/HOL4/Manual/Reference/
H A Dpreface.tex3 This volume is the reference manual for the \HOL\ system.
8 implemented by the \HOL{} system;
10 \item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
18 variable bindings in the \HOL\ system. These include: general-purpose
27 % identifiers in the system except those identifiers that are bound to theorems.
32 from the same database that is used by the help system. For an introduction to
33 the \HOL\ system, see \TUTORIAL; for a systematic presentation, see
H A Dentries-intro.tex4 in the \HOL{} system. These include: general-purpose functions, such
12 The interactive system starts with some structures already present,
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibPortable.sig12 (* Pointer equality using the run-time system *)
H A DmlibPortable.sml23 (* Pointer equality using the run-time system. *)
H A DmlibRewrite.sig23 (* Add an equation into the system *)
29 (* Inter-reduce the equations in the system *)
/seL4-l4v-10.1.1/HOL4/tools/Holmake/tests/Iflag/
H A Dselftest.sml5 val res = OS.Process.system (Systeml.HOLDIR ^ "/bin/Holmake -q -I includethis BTheory.uo 2> /dev/null");
/seL4-l4v-10.1.1/HOL4/src/opentheory/logging/
H A DCurl.sml5 val _ = if isSuccess(system("curl -sSH'Expect:' -F'"^field^"=@"^file^"' '"^url^"' >"^t)) then ()
/seL4-l4v-10.1.1/HOL4/Manual/Description/
H A Dpreface.tex4 This volume contains the description of the \HOL\ system.
9 implemented by the \HOL{} system;
11 \item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
19 prior experience of the system. Beginners should start with the
22 The \HOL\ system is designed to support interactive theorem proving in
39 system of \LOGIC{} is actually implemented in the \ML{} programming
40 language, providing comprehensive descriptions of the system's major
45 the language \ML. That work centred on a system called \LCF\ (logic for
50 logic. The \HOL\ system is a direct descendant of \LCF; this is reflected in
60 \LCF'. The \HOL\ system i
[all...]
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DPrintBdd.sml49 Process.system("dot -G"^glab^" -G"^gsize^" -Tps "^file^".dot -o "^file^".ps");
97 Process.system("sed -f "^file^"_sed_edits "^file^".dot > edited_"^file^".dot");
98 Process.system("dot -G"^glab^" -G"^gsize^" -Tps edited_"^file^".dot -o "^file^".ps");
99 Process.system("rm "^file^".dot");
100 Process.system("rm "^file^"_sed_edits");
101 Process.system("rm edited_"^file^".dot");
/seL4-l4v-10.1.1/HOL4/Manual/Logic/
H A Dpreface.tex4 This volume contains the description of the \HOL\ system's logic. It
9 implemented by the \HOL{} system;
11 \item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
26 The \HOL\ system is designed to support interactive theorem proving in
41 \HOL{} system, and presents it abstractly.
45 and implemented the language \ML. That work centred on a system
51 \HOL\ system is a direct descendant of \LCF; this is reflected in
61 \LCF'. The \HOL\ system is implemented on top of an early version of Cambridge
68 released (in 1988), after the original \HOL\ system had been in use
74 supported version of the system fo
[all...]
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/
H A Dselftest.sml28 Process.system ("rm " ^ (!model_check_temp_file)))
37 Process.system ("rm " ^ (!model_check_temp_file)))
/seL4-l4v-10.1.1/HOL4/tools/Holmake/tests/cheatspotting/
H A Dselftest.sml9 val res = OS.Process.system ("../../../../../bin/Holmake --noqof " ^ s)
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DPortable.sig16 (* Pointer equality using the run-time system. *)
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DPortable.sig16 (* Pointer equality using the run-time system. *)
/seL4-l4v-10.1.1/HOL4/Manual/Tutorial/
H A Dintro.tex4 This chapter describes how to get the \HOL{} system and how to install
5 it. It is generally assumed that some sort of Unix system is being
8 using the system. \HOL{} may be run on PCs running Windows operating
14 The \HOL{} system can be downloaded from \url{http://hol-theorem-prover.org}.
42 {\tt tools} & Source code for building the system & Directory\\
46 {\tt help} & Help files for \HOL{} system & Directory\\
63 by the user. After entering the \HOL{} system (see below), the user
67 \$} or {\small\verb|-|} are system output. Occasionally, system
88 Before beginning you must have a current version of Poly/ML or Moscow~ML.\footnote{We recommend using Poly/ML on all operating systems, but it requires Cygwin or the Windows Linux sub-system o
[all...]
H A Dtheories.tex4 The result of a session with the \HOL{} system is an object called a
19 system provides tools for adding to theories and combining theories.
24 The purpose of the \HOL{} system is to provide tools to enable
27 theory. The \HOL{} system ensures that only well-formed theories can
31 A theory is represented in the \HOL{} system as a collection of SML
42 named in the \HOL{} system by two strings: the name of the theory file
50 A typical piece of work with the \HOL{} system consists in a number of
52 system through its ``command-line interface''. At the same time, it's
57 need to be re-entered into the system. This can be done with
66 the same way as the system'
[all...]
H A Dpreface.tex4 This volume contains a tutorial on the \HOL{} system. It is one of four
9 implemented by the \HOL{} system;
11 \item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
20 and use of the system. The tutorial is intended to give a `hands-on'
35 \item The formal logic supported by the \HOL{} system (higher order
49 \HOL{} system for a tricky proof. Chapter~\ref{chap:combin} is a more
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/
H A Dtheories.tex4 The result of a session with the \HOL{} system is an object called a
19 system provides tools for adding to theories and combining theories.
24 The purpose of the \HOL{} system is to provide tools to enable
27 theory. The \HOL{} system ensures that only well-formed theories can
31 A theory is represented in the \HOL{} system as a collection of SML
42 named in the \HOL{} system by two strings: the name of the theory file
50 A typical piece of work with the \HOL{} system consists in a number of
52 system through its ``command-line interface''. At the same time, it's
57 need to be re-entered into the system. This can be done with
66 the same way as the system'
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/LTL/
H A DCOIRScript.sml65 * A system (similar to a "synchronous circuit" in the book "Model
74 * system is non-deterministic. A deterministic system is one in which
77 * A system is thus a pair (I,E) where I is a set of initial states,
83 * system (I,E). The states are finite maps from strings to values
119 (* Set of all the variables mentioned in a system *)
/seL4-l4v-10.1.1/l4v/camkes/glue-spec/document/
H A Dintro.tex20 report which described the static semantics of component and system
26 component system.
38 of a component system using semantic mechanisms that nevertheless map
51 Similar to how the instantiation of a component system is generated from its
53 the formal specification of a complete \camkes component system from the same
75 C code. A more detailed system is presented in \autoref{h:filter} to
/seL4-l4v-10.1.1/HOL4/tools/
H A Dwin-config.sml52 val _ = print "Configuring the system\n";
54 val _ = Process.system ("mosml < tools\\smart-configure.sml")
75 val _ = print "Building the help system \n";
/seL4-l4v-10.1.1/HOL4/src/thm/
H A DOverlay.sml4 These infix declarations affect the interactive system as well as

Completed in 368 milliseconds

12345678910