| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Rule.sml | 587 fun simplify th = function
|
| H A D | Rule.sig | 242 val simplify : Thm.thm -> Thm.thm option value
|
| H A D | Normalize.sml | 993 datatype simplify = type
1125 fun simplify (Simp {formula,andSet,orSet,xorSet}) = function
|
| H A D | Clause.sml | 213 fun simplify (Clause {parameters,id,thm}) = function
|
| H A D | Clause.sig | 79 val simplify : clause -> clause option value
|
| H A D | Active.sml | 211 type simplify = {subsume : bool, reduce : bool, rewrite : bool}; type
369 fun simplify simp units rewr subs = function
[all...] |
| H A D | Active.sig | 13 type simplify = type
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Rule.sml | 587 fun simplify th = function
|
| H A D | Rule.sig | 242 val simplify : Thm.thm -> Thm.thm option value
|
| H A D | Normalize.sml | 993 datatype simplify = type
1125 fun simplify (Simp {formula,andSet,orSet,xorSet}) = function
|
| H A D | Clause.sml | 213 fun simplify (Clause {parameters,id,thm}) = function
|
| H A D | Clause.sig | 79 val simplify : clause -> clause option value
|
| H A D | Active.sml | 211 type simplify = {subsume : bool, reduce : bool, rewrite : bool}; type
369 fun simplify simp units rewr subs = function
[all...] |
| H A D | Active.sig | 13 type simplify = type
|
| /seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
| H A D | reconstruct.py | 174 def simplify(): function
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
| H A D | CODETREE_SIMPLIFIER.sml | 142 fun simplify(c, s) = mapCodetree (simpGeneral s) c function
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
| H A D | Rules.sml | 35 fun simplify thl = function
|
| H A D | Rules.sig | 24 val simplify : thm list -> thm -> thm value
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibClauseset.sml | 224 fun simplify set = let val SET {rewrites = r, ...} = set in REWRITE r end; function
|
| H A D | mlibClauseset.sig | 33 val simplify : clauseset -> clause -> clause value
|
| H A D | mlibCanon.sml | 65 fun simplify (Not p) = simplify1 (Not (simplify p)) function
[all...] |
| H A D | mlibCanon.sig | 13 val simplify : formula -> formula value
|
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | SolverSpec.sml | 81 fun simplify simp_tac goal = function
|
| /seL4-l4v-10.1.1/HOL4/examples/muddy/ |
| H A D | bdd.sml | 91 val simplify : bdd -> bdd -> bdd = C (app2 (symb "mlbdd_bdd_simplify")) end value
|
| H A D | bdd.sig | 86 val simplify : bdd -> bdd -> bdd value
|