Searched refs:HOL (Results 151 - 175 of 466) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/cbv-lc/
H A DtypesScript.sml17 (* Change some HOL defaults to the style we often use in CakeML.
69 * expressions and states. HOL can't get the termination on it's own, so we
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/
H A Dadder-in-Model.ml11 % This file defines a HOL specification of an adder that mimics the %
29 % The HOL representation of this MODEL specification is: %
/seL4-l4v-10.1.1/HOL4/src/compute/Manual/
H A Ddescription.tex21 think \HOL\ has a programming language, and \ml{CBV\_CONV} is an
46 primitive notion in \HOL, and is slower.
/seL4-l4v-10.1.1/HOL4/src/num/reduce/Manual/
H A Ddescription.tex26 The approach to representing natural number constants in \HOL\ is to provide a
97 \noindent This will work only if the \HOL\/ being used has been installed
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A DGlobals.sml106 * At the end of type inference, HOL now guesses names for unconstrained *
113 * At the end of type inference, HOL will guess which instance of an *
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/LTL/
H A DLTLScript.sml681 I've tweaked the original HOL LTL proof to go through using the
706 HOL version (i.e. so no need to convert "s IN M.S" to "s IN S M" etc).
712 s-expression representation of a model ``m:sexp`` to a HOL Kripke
713 structures ``MAKE_HOL_MODEL m`` which has HOL type
716 L, R into a HOL record structure:
727 The HOL Theorem1:
744 To link the Sandip and HOL formulations of Kripke structure models one
773 below, plus ACL2 theorems we can import into HOL to prove this (in the
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dsexp.sml2 (* Various ML tools to support ACL2 in HOL including: *)
4 (* 1. A printer from HOL to ACL2. *)
8 (* to HOL term. *)
97 (* Error reporting function (uses some HOL boilerplate I don't understand) *)
201 (* 3. Uses the HOL overloading mechanism to introduce "hol_name" *)
203 (* a valid HOL identifier name). *)
282 print "\" defined with HOL name \"";
330 print "\" defined with HOL name \"";
348 (out("; File created from HOL using print_lisp_file on " ^ date() ^ "\n\n");
789 (* a negative integer to HOL representatio
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A Dsexp.sml2 (* Various ML tools to support ACL2 in HOL including: *)
4 (* 1. A printer from HOL to ACL2. *)
8 (* to HOL term. *)
97 (* Error reporting function (uses some HOL boilerplate I don't understand) *)
201 (* 3. Uses the HOL overloading mechanism to introduce "hol_name" *)
203 (* a valid HOL identifier name). *)
282 print "\" defined with HOL name \"";
330 print "\" defined with HOL name \"";
348 (out("; File created from HOL using print_lisp_file on " ^ date() ^ "\n\n");
789 (* a negative integer to HOL representatio
[all...]
H A Dhol_defaxioms_thmsScript.sml2 (* HOL proofs of defthms in defaxioms.lisp.trans. *)
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/
H A Dappendix0.tex157 \caption{Reserved Words in HOL Terms}
188 %\caption{Minor Keywords in HOL Theories}
H A Dadvanced0.tex32 %proof time. In HOL you may have to work hard to define a function, but proofs
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/
H A Dappendix0.tex157 \caption{Reserved Words in HOL Terms}
188 %\caption{Minor Keywords in HOL Theories}
H A Dadvanced0.tex32 %proof time. In HOL you may have to work hard to define a function, but proofs
/seL4-l4v-10.1.1/HOL4/help/src-sml/
H A DHOLPage.sml95 \<HEAD><TITLE>HOL Reference Page</TITLE></HEAD>\n";
97 out "<H1>HOL Reference Page</H1>\n";
/seL4-l4v-10.1.1/l4v/spec/abstract/document/
H A Droot.tex143 Isabelle/HOL specification of the seL4 microkernel. It is
147 text generated from the formal Isabelle/HOL definitions.
/seL4-l4v-10.1.1/l4v/proof/bisim/document/
H A Droot.tex126 %Isabelle/HOL specification of the seL4 microkernel. It is
130 %text generated from the formal Isabelle/HOL definitions.
/seL4-l4v-10.1.1/HOL4/examples/dev/Fact32/
H A DFact32.ml106 (* Stop zillions of warning messages that HOL variables of type ``:num`` *)
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/
H A Dvalues.ml1 % MICROCODED COMPUTER PROOF : HOL %
/seL4-l4v-10.1.1/HOL4/src/1/
H A DThm_cont.sml3 (* DESCRIPTION : Larry Paulson's theorem continuations for HOL. *)
178 * DISCH changed to NEG_DISCH for HOL
202 * ported from John Harrison's HOL Light *
338 (* This version deleted for HOL version 1.12 [TFM 91.01.17] *)
/seL4-l4v-10.1.1/HOL4/src/HolSat/
H A DsatConfig.sml22 flags : {is_cnf:bool,is_proved:bool} (* problem already in cnf, result is checked in HOL *)
/seL4-l4v-10.1.1/HOL4/src/holyhammer/
H A DholyHammer.sig72 (* Export HOL4 library to Holyhammer infrastructure in HOL/Light *)
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmetisTools.sig2 (* A HOL INTERFACE TO THE METIS FIRST-ORDER PROVER. *)
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DTravrules.sml6 * Based loosely on original HOL rewriting by
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/
H A DrelScript.sml73 (* The HOL type we use to model relations. *)
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DVarmap.sml42 (* as numbers) to HOL variables. Variable maps are represented as *)

Completed in 230 milliseconds

1234567891011>>