| /seL4-l4v-master/HOL4/Manual/Description/ |
| H A D | QuantHeuristics.tex | 42 \textbf{Problem} & \textbf{Result} \\\hline
|
| /seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
| H A D | QuantHeuristics.tex | 42 \textbf{Problem} & \textbf{Result} \\\hline
|
| /seL4-l4v-master/HOL4/examples/HolBdd/ |
| H A D | MachineTransitionScript.sml | 1013 (* Problem with Q.SPECL? Too many type annotations needed. *)
|
| /seL4-l4v-master/HOL4/examples/hardware/hol88/cmos/ |
| H A D | mk_DYN_ADD.ml | 3 the Stuck-open Fault Problem of Testability" by A. F. Murray
|
| /seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
| H A D | LK.tex | 456 can be solved automatically. Problem~39 concerns set theory, asserting
|
| /seL4-l4v-master/isabelle/src/Tools/Metis/ |
| H A D | Makefile | 74 src/Problem.sig src/Problem.sml \
|
| /seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
| H A D | Problem.sig | 6 signature Problem = signature
|
| H A D | Problem.sml | 6 structure Problem :> Problem = structure
|
| H A D | Tptp.sig | 183 Problem of
199 problem : Problem.problem} -> problem
204 problem : Problem.problem,
|
| H A D | Tptp.sml | 1768 Problem of
1773 fun hasCnfConjecture (Problem {formulas,...}) =
1776 fun hasFofConjecture (Problem {formulas,...}) =
1779 fun hasConjecture (Problem {formulas,...}) =
1782 fun freeVars (Problem {formulas,...}) = freeVarsListFormula formulas;
1831 Problem
1839 {problem : Problem.problem,
2009 fun goal (Problem {formulas,...}) =
2030 fun normalize (Problem {formulas,...}) =
2110 Problem
2142 val Problem {comments,includes,formulas} = problem value
2540 val Problem {formulas,...} = problem value
[all...] |
| H A D | metis.sml | 164 else TextIO.print ("Problem: " ^ filename ^ "\n\n");
177 else TextIO.print ("Clauses:\n" ^ Problem.toString cls ^ "\n\n");
186 val {clauses,literals,symbols,typedSymbols} = Problem.size cls
200 val cat = Problem.categorize cls
202 TextIO.print ("Category: " ^ Problem.categoryToString cat ^ ".\n\n")
221 Tptp.Problem
355 val Tptp.Problem {includes = i, formulas = f, ...} =
369 val Tptp.Problem {comments,includes,formulas} = problem
380 Tptp.Problem
|
| H A D | problems2tptp.sml | 15 (* Problem data. *)
80 Tptp.Problem
|
| H A D | selftest.sml | 36 (* Problem data. *)
|
| /seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/ |
| H A D | LK.tex | 456 can be solved automatically. Problem~39 concerns set theory, asserting
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/ |
| H A D | Makefile | 74 src/Problem.sig src/Problem.sml \
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Problem.sig | 6 signature Problem = signature
|
| H A D | Problem.sml | 6 structure Problem :> Problem = structure
|
| H A D | Tptp.sig | 183 Problem of
199 problem : Problem.problem} -> problem
204 problem : Problem.problem,
|
| H A D | Tptp.sml | 1768 Problem of
1773 fun hasCnfConjecture (Problem {formulas,...}) =
1776 fun hasFofConjecture (Problem {formulas,...}) =
1779 fun hasConjecture (Problem {formulas,...}) =
1782 fun freeVars (Problem {formulas,...}) = freeVarsListFormula formulas;
1831 Problem
1839 {problem : Problem.problem,
2009 fun goal (Problem {formulas,...}) =
2030 fun normalize (Problem {formulas,...}) =
2110 Problem
2142 val Problem {comments,includes,formulas} = problem value
2540 val Problem {formulas,...} = problem value
[all...] |
| H A D | metis.sml | 164 else TextIO.print ("Problem: " ^ filename ^ "\n\n");
177 else TextIO.print ("Clauses:\n" ^ Problem.toString cls ^ "\n\n");
186 val {clauses,literals,symbols,typedSymbols} = Problem.size cls
200 val cat = Problem.categorize cls
202 TextIO.print ("Category: " ^ Problem.categoryToString cat ^ ".\n\n")
221 Tptp.Problem
355 val Tptp.Problem {includes = i, formulas = f, ...} =
369 val Tptp.Problem {comments,includes,formulas} = problem
380 Tptp.Problem
|
| H A D | problems2tptp.sml | 15 (* Problem data. *)
80 Tptp.Problem
|
| H A D | selftest.sml | 36 (* Problem data. *)
|
| /seL4-l4v-master/HOL4/examples/AKS/compute/ |
| H A D | computeParamScript.sml | 303 (* Problem: Given n and m, find the smallest k such that ordz k n > m *)
|
| /seL4-l4v-master/HOL4/examples/HolBdd/Examples/KatiPuzzle/ |
| H A D | KatiPuzzleScript.sml | 20 (* Problem is whether one can get from *)
|
| /seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
| H A D | polyRingScript.sml | 2968 (* Problem 1: establish degree of polynomial addition. *)
3001 (* Problem 2: establish degree of polynomial multiplication. *)
3258 (* Problem 3: establish polynomial leads for addition and multiplication. *)
4216 (* Problem 4: establish polynomial division algorithm: *)
|