| /seL4-l4v-10.1.1/HOL4/Manual/Logic/ |
| H A D | semantics.tex | 848 is not allowed as a constant definition. The problem is that the
1069 Section~\ref{defs}. In a sense, what is causing the problem in the
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | HolSat.tex | 152 A special value \texttt{base\_config~:~sat\_config} is provided for which the term is \texttt{T}, the solver is MiniSat, the options are unset, the CNF flag is false and the proof flag is true. This value can be inspected and modified using getter and setter functions provided in \texttt{src/HolSat/satConfig.sig}. For example, to invoke ZChaff (assuming it is installed), on a file \texttt{unsat.cnf} containing an unsatisfiable problem, we do:
168 If the problem were satisfiable, the model can be captured via exception, as shown earlier.
179 a CNF \HOL{} term corresponding to the SAT problem in the file named by {\it file}. Since DIMACS uses numbers to denote variables, and numbers are not legal identifiers in \HOL{}, each variable number is prefixed with the string ``{\tt v}''. This string is defined in the reference variable {\tt dimacsTools.prefix} and can be changed if required. This function can be used independently of {\tt{HolSatLib}} to read in DIMACS format files.
|
| H A D | conv.tex | 257 There is a similar problem with the tactical {\tt REPEAT}; see
|
| H A D | libraries.tex | 1888 goals, revealing the kernel of the problem. On the other hand, this
|
| H A D | tactics.tex | 221 the \HOL{} user in this case is that the problem may be not
1432 raises the more general problem of denoting\index{assumptions!denoting of, in proofs}\index{denoting assumptions} assumptions in the first place.
1783 \noindent The problem is now to combine the two assumptions to produce the
1889 A more serious problem is that order-sensitive tactics are meaningful
2127 \index{failure, of tactics} a particularly difficult problem to
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/binomial/ |
| H A D | binomial.tex | 440 method is fine for small proofs, but in larger proofs it presents the problem
|
| /seL4-l4v-10.1.1/HOL4/Manual/Tutorial/binomial/ |
| H A D | binomial.tex | 440 method is fine for small proofs, but in larger proofs it presents the problem
|
| /seL4-l4v-10.1.1/HOL4/developers/discussion/ |
| H A D | overloading-extension.tex | 101 To figure out whether the latter is safe or not is the problem of
103 problem that Steven Obua's paper~\cite{Obua-RTA06} solves. If we
105 avoid this problem because we can just check each monomorphic
143 problem.
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
| H A D | priv_constraints_cpsr_pcScript.sml | 13 (**** the problem: vector table is based on mode not exception type ******)
|
| /seL4-l4v-10.1.1/HOL4/examples/CCS/ |
| H A D | ExpansionScript.sml | 970 * [3] Sangiorgi, D., Milner, R.: The problem of ���Weak Bisimulation up to.��� CONCUR'92. (1992).
|
| H A D | selftest.sml | 19 fun CCS_TRANS_test (problem, result) = let
22 val p_s = padr 30 (term_to_string problem);
29 problem
|
| /seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
| H A D | DerivedBddRules.sml | 526 val _ = if null tyl then () else (print "type match problem\n";
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | muCheck.sml | 834 problem with EG is that right now it will giv the shortest path it can find, whereas I feel that
838 any initial state. This is not possible in theory, so points to some problem with the ce machinery*)
|
| /seL4-l4v-10.1.1/HOL4/examples/PSL/experimental-semantics/ |
| H A D | SERE.ml | 160 (* The problem with fusion is that if w is a weak word that matches *)
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
| H A D | acl2_packageScript.sml | 70 (* rewriting the big term is no problem, but compiling it breaks. *)
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
| H A D | acl2_packageScript.sml | 70 (* rewriting the big term is no problem, but compiling it breaks. *)
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | acl2_packageScript.sml | 70 (* rewriting the big term is no problem, but compiling it breaks. *)
|
| H A D | make_sexp.ml | 758 (* rewriting the big term is no problem, but compiling it breaks. *)
|
| /seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/doc/ |
| H A D | ds.tex | 459 This leaves the problem that a constraint that the set $\values$ is infinite
|
| H A D | presentation-content.tex | 303 \item problem: this is a real implication, information is lost
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | ILScript.sml | 141 (* up to avoid this problem *)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | ILScript.sml | 141 (* up to avoid this problem *)
|
| /seL4-l4v-10.1.1/HOL4/examples/lambda/barendregt/ |
| H A D | standardisationScript.sml | 8 Poly/ML doesn't have this problem. *)
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
| H A D | lisp_semanticsScript.sml | 181 (* having VarBind only partially specified is no problem, but *)
|
| /seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
| H A D | ho_proverTools.sml | 1354 (* Simple strip tac to reduce the problem before beginning *)
|