/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | selftest.sml | 36 (* Problem data. *)
|
H A D | problems2tptp.sml | 15 (* Problem data. *) 80 Tptp.Problem
|
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 | 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 | Tptp.sig | 183 Problem of 199 problem : Problem.problem} -> problem 204 problem : Problem.problem,
|
H A D | Problem.sml | 6 structure Problem :> Problem = structure
|
H A D | Problem.sig | 6 signature Problem = signature
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | selftest.sml | 36 (* Problem data. *)
|
H A D | problems2tptp.sml | 15 (* Problem data. *) 80 Tptp.Problem
|
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 | 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 | Tptp.sig | 183 Problem of 199 problem : Problem.problem} -> problem 204 problem : Problem.problem,
|
H A D | Problem.sml | 6 structure Problem :> Problem = structure
|
H A D | Problem.sig | 6 signature Problem = signature
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/ |
H A D | Makefile | 74 src/Problem.sig src/Problem.sml \
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/ |
H A D | Makefile | 74 src/Problem.sig src/Problem.sml \
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 1054 \subsection{Problem Encoding}
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 1054 \subsection{Problem Encoding}
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 456 can be solved automatically. Problem~39 concerns set theory, asserting
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 456 can be solved automatically. Problem~39 concerns set theory, asserting
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | trace_refute.py | 130 p = problem.Problem (None, name = ', '.join(fnames)) 349 p = functions[f].as_problem (problem.Problem) 374 p = functions[fname].as_problem (problem.Problem) 399 p = functions[fname].as_problem (problem.Problem)
|
H A D | syntax.py | 846 def as_problem (self, Problem, name = 'temp'): 847 p = Problem(None, 'Function (%s)' % self.name) 859 def compile_hints (self, Problem): 862 p = self.as_problem (Problem)
|
H A D | stack_logic.py | 640 p = fun.as_problem (problem.Problem, name = 'Target') 728 p = fun.as_problem (problem.Problem, name = 'Target') 881 p = problem.Problem (None, name = 'Recursion Test')
|
H A D | problem.py | 23 class Problem: class in inherits: 27 self.name = 'Problem (%s)' % name 371 ss = ['Problem'] 486 assert lines[0] == 'Problem', lines[0] 490 p = Problem (pairing = None, name = name) 745 trace ('Problem size now %d' % len(p.nodes)) 793 p = f.as_problem (Problem)
|
H A D | loop_bounds.py | 655 p = functions[fname].as_problem (problem.Problem) 764 p = functions[fname].as_problem (problem.Problem) 882 p = fun.as_problem (problem.Problem)
|