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 D | typesScript.sml | 17 (* 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 D | adder-in-Model.ml | 11 % 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 D | description.tex | 21 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 D | description.tex | 26 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 D | Globals.sml | 106 * 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 D | LTLScript.sml | 681 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 D | sexp.sml | 2 (* 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 D | sexp.sml | 2 (* 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 D | hol_defaxioms_thmsScript.sml | 2 (* HOL proofs of defthms in defaxioms.lisp.trans. *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | appendix0.tex | 157 \caption{Reserved Words in HOL Terms} 188 %\caption{Minor Keywords in HOL Theories}
|
H A D | advanced0.tex | 32 %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 D | appendix0.tex | 157 \caption{Reserved Words in HOL Terms} 188 %\caption{Minor Keywords in HOL Theories}
|
H A D | advanced0.tex | 32 %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 D | HOLPage.sml | 95 \<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 D | root.tex | 143 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 D | root.tex | 126 %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 D | Fact32.ml | 106 (* Stop zillions of warning messages that HOL variables of type ``:num`` *)
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/ |
H A D | values.ml | 1 % MICROCODED COMPUTER PROOF : HOL %
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Thm_cont.sml | 3 (* 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 D | satConfig.sml | 22 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 D | holyHammer.sig | 72 (* Export HOL4 library to Holyhammer infrastructure in HOL/Light *)
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | metisTools.sig | 2 (* A HOL INTERFACE TO THE METIS FIRST-ORDER PROVER. *)
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Travrules.sml | 6 * Based loosely on original HOL rewriting by
|
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
H A D | relScript.sml | 73 (* The HOL type we use to model relations. *)
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
H A D | Varmap.sml | 42 (* as numbers) to HOL variables. Variable maps are represented as *)
|
Completed in 230 milliseconds
1234567891011>>