| /seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
| H A D | Problem.sml | 54 val fm = Formula.False value
55 val fm = value
58 val fm = Formula.Imp (clsToFm axioms, fm) value
|
| H A D | selftest.sml | 627 val fm = LiteralSet.disjoin cl value
|
| H A D | Normalize.sml | 393 val fm = applyPolarity p fm value
409 val fm = value
474 val fm = Set.pick sv value
512 val fm = Set.pick sv value
588 val fm = subst_domain sub domain fvSub fm value
639 val fm = lastElt s value
767 val fm = cnfFm avoid fm value
956 val (fm,inf) = destThm th value
1144 val fm = AndSet s value
1154 val fm = OrSet s value
1164 val fm = XorPolaritySet (p,s) value
1262 val fm = Formula.Iff (Formula.Atom atm, toFormula def) value
1263 val fm = Formula.setMkForall (fv,fm) value
1266 val fm = Xor2 (lit,def) value
1342 val fm = basicCnf fm value
[all...] |
| H A D | Tptp.sml | 2013 val fm = value
2019 val fm = value
2023 val fm = value
2217 val (fm,_) = Normalize.destThm th value
2334 val (fm,pars) = subgoal value
2499 val fm = Formula.Not fm value
[all...] |
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Problem.sml | 54 val fm = Formula.False value
55 val fm = value
58 val fm = Formula.Imp (clsToFm axioms, fm) value
|
| H A D | selftest.sml | 627 val fm = LiteralSet.disjoin cl value
|
| H A D | Normalize.sml | 393 val fm = applyPolarity p fm value
409 val fm = value
474 val fm = Set.pick sv value
512 val fm = Set.pick sv value
588 val fm = subst_domain sub domain fvSub fm value
639 val fm = lastElt s value
767 val fm = cnfFm avoid fm value
956 val (fm,inf) = destThm th value
1144 val fm = AndSet s value
1154 val fm = OrSet s value
1164 val fm = XorPolaritySet (p,s) value
1262 val fm = Formula.Iff (Formula.Atom atm, toFormula def) value
1263 val fm = Formula.setMkForall (fv,fm) value
1266 val fm = Xor2 (lit,def) value
1342 val fm = basicCnf fm value
[all...] |
| H A D | Tptp.sml | 2013 val fm = value
2019 val fm = value
2023 val fm = value
2217 val (fm,_) = Normalize.destThm th value
2334 val (fm,pars) = subgoal value
2499 val fm = Formula.Not fm value
[all...] |
| /seL4-l4v-master/HOL4/examples/PSL/1.01/parser/ |
| H A D | ParserTools.sml | 339 val fm = parseFl f value
|
| /seL4-l4v-master/HOL4/examples/ |
| H A D | dpll.sml | 205 val fm = value
|
| /seL4-l4v-master/HOL4/src/finite_maps/ |
| H A D | flookupLib.sml | 243 val fm = Lib.with_exn (fst o finite_mapSyntax.dest_flookup) tm err value
|
| H A D | fmapalTacs.sml | 541 let val (fm, pair) = dest_binop value
586 let val (fm, pair) = dest_binop value
|
| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | mlibCanon.sml | 222 val fm = list_mk_conj fms value
[all...] |
| H A D | mlibSupport.sml | 156 val fm = clause_to_formula cl value
[all...] |
| /seL4-l4v-master/HOL4/examples/lambda/basics/ |
| H A D | termScript.sml | 630 val fm = mk_exists(v,concl c1) value
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/decompiler/ |
| H A D | decompilerLib.sml | 148 val (fm,tm) = dest_eq tm value
|