| /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/isabelle/src/Tools/Metis/src/ |
| H A D | Active.sig | 13 type simplify = type
|
| H A D | Clause.sig | 79 val simplify : clause -> clause option value
|
| H A D | Clause.sml | 213 fun simplify (Clause {parameters,id,thm}) = function
|
| H A D | Rule.sig | 242 val simplify : Thm.thm -> Thm.thm 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 | Rule.sml | 587 fun simplify th = function
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Active.sig | 13 type simplify = type
|
| H A D | Clause.sig | 79 val simplify : clause -> clause option value
|
| H A D | Clause.sml | 213 fun simplify (Clause {parameters,id,thm}) = function
|
| H A D | Rule.sig | 242 val simplify : Thm.thm -> Thm.thm 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 | Rule.sml | 587 fun simplify th = function
|
| /seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
| H A D | Rules.sig | 24 val simplify : thm list -> thm -> thm value
|
| H A D | Rules.sml | 35 fun simplify thl = function
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibCanon.sig | 13 val simplify : formula -> formula value
|
| 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 | mlibClauseset.sml | 224 fun simplify set = let val SET {rewrites = r, ...} = set in REWRITE r end; function
|
| /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/examples/elliptic/ |
| H A D | elliptic_exampleScript.sml | 44 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
96 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
103 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
116 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
|
| H A D | ellipticScript.sml | 60 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
674 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
682 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
690 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
698 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
706 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
714 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1138 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1152 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1183 val {simplify value
1218 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1230 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1242 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1263 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1311 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1320 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1419 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1422 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1431 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1439 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1452 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
[all...] |
| H A D | groupScript.sml | 53 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
552 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
560 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
568 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
577 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
597 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
605 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
613 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
621 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
629 val {simplify value
638 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
698 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
725 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
748 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
768 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
801 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
821 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
849 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
862 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
890 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
932 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
943 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
953 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1074 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1136 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1427 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1449 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
1515 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/muddy/ |
| H A D | bdd.sig | 86 val simplify : bdd -> bdd -> bdd value
|
| H A D | bdd.sml | 91 val simplify : bdd -> bdd -> bdd = C (app2 (symb "mlbdd_bdd_simplify")) end value
|