| /seL4-l4v-10.1.1/HOL4/Manual/Interaction/ |
| H A D | Makefile | 2 pdflatex HOL-interaction.tex
3 pdflatex HOL-interaction.tex
6 rm -f *.log *.aux HOL-interaction.pdf
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Prog_Prove/document/ |
| H A D | build | 8 isabelle logo HOL
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Prog_Prove/document/ |
| H A D | build | 8 isabelle logo HOL
|
| /seL4-l4v-10.1.1/isabelle/src/HOL/TPTP/lib/Tools/ |
| H A D | tptp_isabelle | 27 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
34 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| H A D | tptp_isabelle_hot | 27 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
34 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| H A D | tptp_nitpick | 27 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
34 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| H A D | tptp_refute | 26 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
33 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| H A D | tptp_sledgehammer | 27 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
34 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| H A D | tptp_translate | 26 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
31 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/HOL/TPTP/lib/Tools/ |
| H A D | tptp_isabelle | 27 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
34 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| H A D | tptp_isabelle_hot | 27 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
34 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| H A D | tptp_nitpick | 27 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
34 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| H A D | tptp_refute | 26 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
33 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| H A D | tptp_sledgehammer | 27 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
34 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| H A D | tptp_translate | 26 isabelle build -b HOL-TPTP 2>&1 | grep --line-buffered -v "elapsed time$"
31 isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^poly.*warning: The type of\|^ monotype.$"
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ |
| H A D | .acl2holrc.bash | 9 export ACL2_HOL=/home/mk606/hol/HOL/examples/acl2
13 export ACL2_HOL=/u/kaufmann/projects/HOL/examples/acl2
17 export ACL2_HOL=/Users/kaufmann/projects/HOL/examples/acl2
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | folMapping.sig | 2 (* MAPPING BETWEEN HOL AND FIRST-ORDER LOGIC. *)
21 with_types : bool}; (* First-order terms include HOL type info *)
27 (* Mapping HOL literals to FOL (need to pass in variables) *)
30 (* Mapping HOL theorems to FOL axioms *)
33 (* Mapping FOL theorems to HOL *)
39 (* Prettify FOL representations of HOL terms---WILL BREAK PROOF TRANSLATION! *)
|
| /seL4-l4v-10.1.1/HOL4/src/Boolify/test/ |
| H A D | Makefile | 4 HOL=hol.bare.unquote -I ../src macro
15 @grep -v 'HOL.* (built \|^\(- \)*runtime: \|User: ' <result.ok >$(TMPFILE1)
16 @grep -v 'HOL.* (built \|^\(- \)*runtime: \|User: ' <result >$(TMPFILE2)
21 $(HOL) <test.sml 2>&1 | tee result
|
| /seL4-l4v-10.1.1/HOL4/examples/pgcl/examples/ |
| H A D | Makefile | 6 HOL = ../../../bin/hol.bare macro
21 $(HOL) <verification.sml | tee verification-log
|
| /seL4-l4v-10.1.1/HOL4/Manual/Reference/ |
| H A D | preface.tex | 3 This volume is the reference manual for the \HOL\ system.
4 It is one of four documents making up the documentation for \HOL:
8 implemented by the \HOL{} system;
9 \item \TUTORIAL: a tutorial introduction to \HOL, with case studies;
10 \item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
11 \item \REFERENCE: the reference manual for \HOL.
18 variable bindings in the \HOL\ system. These include: general-purpose
21 and terms of the \HOL\ logic, for setting up theories, and for using the
33 the \HOL\ system, see \TUTORIAL; for a systematic presentation, see
|
| /seL4-l4v-10.1.1/HOL4/Manual/Logic/ |
| H A D | preface.tex | 4 This volume contains the description of the \HOL\ system's logic. It
5 is one of four volumes making up the documentation for \HOL:
9 implemented by the \HOL{} system;
10 \item \TUTORIAL: a tutorial introduction to \HOL, with case studies;
11 \item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
12 \item \REFERENCE: the reference manual for \HOL.
22 systems (HOL~Light, ProofPower), and is similar to that implemented in
23 Isabelle, where it is called Isabelle/HOL, it is now presented in its
26 The \HOL\ system is designed to support interactive theorem proving in
27 higher order logic (hence the acronym `\HOL')
[all...] |
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Logic/ |
| H A D | preface.tex | 4 Questo volume contiene la descrizione della logica del sistema \HOL. E'
5 uno di quattro volumi che compongono la documentazione per \HOL:
9 implementata dal sistema \HOL{}.
10 \item \TUTORIAL: un tutorial d'introduzione a \HOL, con dei casi di studio.
11 \item \DESCRIPTION: una guida utente dettagliata per il sistema \HOL{}.
12 \item \REFERENCE: il manuale di riferimento per \HOL.
22 di teoremi (HOL~Light, ProofPower), ed � simile a quella implementata in
23 Isabelle, in cui � chiamata Isabelle/HOL, ora � presentata nel suo
26 Il sistema \HOL\ � sviluppato per supportare la dimostrazione interattiva di teoremi nella
27 logica di ordine superiore(da qui l'acronimo `\HOL')
[all...] |
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | preface.tex | 4 This volume contains the description of the \HOL\ system.
5 It is one of four volumes making up the documentation for \HOL:
9 implemented by the \HOL{} system;
10 \item \TUTORIAL: a tutorial introduction to \HOL, with case studies;
11 \item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
12 \item \REFERENCE: the reference manual for \HOL.
22 The \HOL\ system is designed to support interactive theorem proving in
23 higher order logic (hence the acronym `\HOL'). To this end, the formal
27 The version of higher order logic used in \HOL\ is predicate calculus
30 \cite{Church}. The primary application area of \HOL\ wa
[all...] |
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | preface.tex | 4 Questo volume contiene la descrizione del sistema \HOL.
5 E' uno di quattro volumi che compongono la documentazione per \HOL:
9 implementata dal sistema \HOL{}.
10 \item \TUTORIAL: un tutorial d'introduzione a \HOL, con dei casi di studio.
11 \item \DESCRIPTION: una guida utente dettagliata per il sistema \HOL{}.
12 \item \REFERENCE: il manuale di riferimento per \HOL.
22 Il sistema \HOL\ � sviluppato per supportare la dimostrazione interattiva di teoremi nella
23 logica di ordine superiore (da qui l'acronimo `\HOL' [Higher Order Logic (ndt)]). A questo scopo, la logica
27 La versione della logica di ordine superiore usata in \HOL\ � il calcolo dei predicati
30 \cite{Church}. La principale area di applicazione di \HOL\ f
[all...] |
| /seL4-l4v-10.1.1/HOL4/Manual/Tutorial/ |
| H A D | preface.tex | 4 This volume contains a tutorial on the \HOL{} system. It is one of four
5 documents making up the documentation for \HOL:
9 implemented by the \HOL{} system;
10 \item \TUTORIAL: a tutorial introduction to \HOL, with case studies;
11 \item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
12 \item \REFERENCE: the reference manual for \HOL.
19 users of \HOL. It provides a self-study introduction to the structure
21 feel for the way \HOL{} is used, but it does not systematically
24 capable of using \HOL\ for simple tasks, and should also be in a
29 Chapter~\ref{install} explains how to get and install \HOL
[all...] |