| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
| H A D | ml_bind.sml | 27 structure cl = Class structure
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibKernel.sml | 55 let val cl = rev (setify (clause th)) value
65 val cl = cl1' @ cl2' value
[all...] |
| H A D | mlibResolution.sml | 168 val cl = if order_stickiness <= 2 then mlibClause.drop_order cl els value
182 val cl = mlibClause.FRESH_VARS cl value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/KatiPuzzle/ |
| H A D | KatiPuzzleScript.sml | 203 let val cl = strip_pair tm value
|
| /seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/ |
| H A D | HexSolitaireScript.sml | 187 let val cl = strip_pair tm value
|
| H A D | SolitaireScript.sml | 230 let val cl = strip_pair tm value
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | holCheckTools.sml | 41 val cl = List.length (strip_pair state) value
|
| H A D | stringBinTree.sml | 66 val cl = List.foldl (fn (k,acl) => List.foldr value
[all...] |
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Thm.sml | 209 val cl = LiteralSet.fromList [eqLit, Literal.negate lit, lit'] value
[all...] |
| H A D | Active.sml | 388 val cl = if r then Clause.reduce units cl else cl value
901 val cl = Clause.freshVars cl value
[all...] |
| H A D | Clause.sml | 310 val cl = Clause {parameters = parameters, id = newId (), thm = th} value
[all...] |
| H A D | Proof.sml | 110 val cl = Thm.clause th value
312 val cl = Thm.clause th value
359 val cl = Thm.clause th value
376 val cl = Thm.clause th value
[all...] |
| H A D | Subsume.sml | 262 val cl = clauseSym (LiteralSet.toList cl) value
[all...] |
| H A D | selftest.sml | 649 val cl = LS[`$x = $x`]; value
651 val cl = LS[`~($x = $y)`,`$y = $x`]; value
653 val cl = LS[`~($x = $y)`,`~($y = $z)`,`$x = $z`]; value
658 val cl = LS[`project1 $x1 = $x1`]; value
660 val cl = LS[`project1 $x1 $x2 = $x1`]; value
662 val cl = LS[`project2 $x1 $x2 = $x2`]; value
664 val cl = LS[`project1 $x1 $x2 $x3 = $x1`]; value
666 val cl = LS[`project2 $x1 $x2 $x3 = $x2`]; value
668 val cl = LS[`project3 $x1 $x2 $x3 = $x3`]; value
670 val cl = LS[`project1 $x1 $x2 $x3 $x4 = $x1`]; value
672 val cl = LS[`project2 $x1 $x2 $x3 $x4 = $x2`]; value
674 val cl = LS[`project3 $x1 $x2 $x3 $x4 = $x3`]; value
676 val cl = LS[`project4 $x1 $x2 $x3 $x4 = $x4`]; value
678 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 = $x1`]; value
680 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 = $x2`]; value
682 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 = $x3`]; value
684 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 = $x4`]; value
686 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 = $x5`]; value
688 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 = $x1`]; value
690 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 = $x2`]; value
692 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 = $x3`]; value
694 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 = $x4`]; value
696 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 = $x5`]; value
698 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 = $x6`]; value
700 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x1`]; value
702 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x2`]; value
704 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x3`]; value
706 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x4`]; value
708 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x5`]; value
710 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x6`]; value
712 val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x7`]; value
714 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x1`]; value
716 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x2`]; value
718 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x3`]; value
720 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x4`]; value
722 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x5`]; value
724 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x6`]; value
726 val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x7`]; value
728 val cl = LS[`project8 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x8`]; value
730 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x1`]; value
732 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x2`]; value
734 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x3`]; value
736 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x4`]; value
738 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x5`]; value
740 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x6`]; value
742 val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x7`]; value
744 val cl = LS[`project8 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x8`]; value
746 val cl = LS[`project9 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x9`]; value
752 val cl = LS[`~isZero $x`,`$x = 0`]; value
754 val cl = LS[`isZero $x`,`~($x = 0)`]; value
758 val cl = LS[`0 + 1 = 1`]; value
760 val cl = LS[`1 + 1 = 2`]; value
762 val cl = LS[`2 + 1 = 3`]; value
764 val cl = LS[`3 + 1 = 4`]; value
766 val cl = LS[`4 + 1 = 5`]; value
768 val cl = LS[`5 + 1 = 6`]; value
770 val cl = LS[`6 + 1 = 7`]; value
772 val cl = LS[`7 + 1 = 8`]; value
774 val cl = LS[`8 + 1 = 9`]; value
776 val cl = LS[`9 + 1 = 10`]; value
780 val cl = LS[`~1 = negative1`]; value
782 val cl = LS[`~2 = negative2`]; value
784 val cl = LS[`~3 = negative3`]; value
786 val cl = LS[`~4 = negative4`]; value
788 val cl = LS[`~5 = negative5`]; value
790 val cl = LS[`~6 = negative6`]; value
792 val cl = LS[`~7 = negative7`]; value
794 val cl = LS[`~8 = negative8`]; value
796 val cl = LS[`~9 = negative9`]; value
798 val cl = LS[`~10 = negative10`]; value
802 val cl = LS[`0 + $x = $x`]; value
804 val cl = LS[`$x + $y = $y + $x`]; value
806 val cl = LS[`$x + ($y + $z) = ($x + $y) + $z`]; value
810 val cl = LS[`~$x + $x = 0`]; value
812 val cl = LS[`~~$x = $x`]; value
816 val cl = LS[`$x - $y = $x + ~$y`]; value
820 val cl = LS[`suc $x = $x + 1`]; value
824 val cl = LS[`pre $x = $x - 1`]; value
828 val cl = LS[`$x <= $x`]; value
830 val cl = LS[`~($x <= $y)`,`~($y <= $z)`,`$x <= $z`]; value
832 val cl = LS[`~($x <= $y)`,`~($y <= $x)`,`$x = $y`]; value
834 val cl = LS[`0 <= $x`]; value
836 val cl = LS[`~($x >= $y)`,`$y <= $x`]; value
838 val cl = LS[`$x >= $y`,`~($y <= $x)`]; value
840 val cl = LS[`$x > $y`,`$x <= $y`]; value
842 val cl = LS[`~($x > $y)`,`~($x <= $y)`]; value
844 val cl = LS[`$x < $y`,`$y <= $x`]; value
846 val cl = LS[`~($x < $y)`,`~($y <= $x)`]; value
848 val cl = LS[`$x = 0`,`~($x <= $y)`,`~$y <= ~$x`]; value
852 val cl = LS[`1 * $x = $x`]; value
854 val cl = LS[`0 * $x = 0`]; value
856 val cl = LS[`$x * $y = $y * $x`]; value
858 val cl = LS[`$x * ($y * $z) = ($x * $y) * $z`]; value
860 val cl = LS[`$x * ($y + $z) = ($x * $y) + ($x * $z)`]; value
862 val cl = LS[`$x * ~$y = ~($x * $y)`]; value
866 val cl = LS[`$y = 0`,`$x mod $y < $y`]; value
868 val cl = LS[`$y * ($x div $y) + $x mod $y = $x`]; value
872 val cl = LS[`exp $x 0 = 1`]; value
874 val cl = LS[`$y = 0`,`exp $x $y = $x * exp $x (pre $y)`]; value
878 val cl = LS[`divides $x $x`]; value
880 val cl = LS[`~(divides $x $y)`,`~(divides $y $z)`,`divides $x $z`]; value
882 val cl = LS[`~(divides $x $y)`,`~(divides $y $x)`,`$x = $y`]; value
884 val cl = LS[`divides 1 $x`]; value
886 val cl = LS[`divides $x 0`]; value
890 val cl = LS[`even 0`]; value
892 val cl = LS[`$x = 0`,`~(even (pre $x))`,`odd $x`]; value
894 val cl = LS[`$x = 0`,`~(odd (pre $x))`,`even $x`]; value
900 val cl = LS[`~member $x empty`]; value
904 val cl = LS[`member $x universe`]; value
908 val cl = LS[`member $x $y`,`member $x (complement $y)`]; value
910 val cl = LS[`~(member $x $y)`,`~member $x (complement $y)`]; value
912 val cl = LS[`complement (complement $x) = $x`]; value
914 val cl = LS[`complement empty = universe`]; value
916 val cl = LS[`complement universe = empty`]; value
920 val cl = LS[`subset $x $x`]; value
922 val cl = LS[`~subset $x $y`,`~subset $y $z`,`subset $x $z`]; value
924 val cl = LS[`~subset $x $y`,`~subset $y $x`,`$x = $y`]; value
926 val cl = LS[`subset empty $x`]; value
928 val cl = LS[`subset $x universe`]; value
930 val cl = LS[`~subset $x $y`,`subset (complement $y) (complement $x)`]; value
932 val cl = LS[`~member $x $y`,`~subset $y $z`,`member $x $z`]; value
936 val cl = LS[`union $x $y = union $y $x`]; value
938 val cl = LS[`union $x (union $y $z) = union (union $x $y) $z`]; value
940 val cl = LS[`union empty $x = $x`]; value
942 val cl = LS[`union universe $x = universe`]; value
944 val cl = LS[`subset $x (union $x $y)`]; value
946 val cl = LS[`~member $x (union $y $z)`,`member $x $y`,`member $x $z`]; value
950 val cl = LS[`intersect $x $y = value
953 val cl = LS[`subset (intersect $x $y) $x`]; value
957 val cl = LS[`difference $x $y = intersect $x (complement $y)`]; value
961 val cl = LS[`symmetricDifference $x $y = value
966 val cl = LS[`member $x (insert $x $y)`]; value
970 val cl = LS[`singleton $x = (insert $x empty)`]; value
974 val cl = LS[`card empty = 0`]; value
976 val cl = LS[`member $x $y`,`card (insert $x $y) = suc (card $y)`]; value
982 val cl = LS[`null nil`]; value
984 val cl = LS[`~null $x`, `$x = nil`]; value
988 val cl = LS[`~(nil = $x :: $y)`]; value
992 val cl = LS[`$x @ ($y @ $z) = ($x @ $y) @ $z`]; value
994 val cl = LS[`nil @ $x = $x`]; value
996 val cl = LS[`$x @ nil = $x`]; value
1000 val cl = LS[`length nil = 0`]; value
1002 val cl = LS[`length ($x :: $y) >= length $y`]; value
1004 val cl = LS[`length ($x @ $y) >= length $x`]; value
1006 val cl = LS[`length ($x @ $y) >= length $y`]; value
1010 val cl = LS[`null $x`,`suc (length (tail $x)) = length $x`]; value
1017 val cl = pvCl (CL[`P $x`,`P $y`]); value
1020 val cl = pvCl (CL[`P $x`,`~P (f $x)`]); value
1022 val cl = pvCl (CL[`$x = $y`,`f $y = f $x`]); value
1024 val cl = pvCl (CL[`$x = f $y`,`f $x = $y`]); value
1026 val cl = pvCl (CL[`s = a`,`s = b`,`h b c`]); value
1028 val cl = pvCl (CL[`a = a`,`a = b`,`h b c`]); value
1063 val cl = pvCl (LcpCL[`~($y <= (2 + (2 * $x + pow $x 2)) / 2)`, `~(0 <= $x)`, value
[all...] |
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Thm.sml | 209 val cl = LiteralSet.fromList [eqLit, Literal.negate lit, lit'] value
[all...] |
| H A D | Active.sml | 388 val cl = if r then Clause.reduce units cl else cl value
901 val cl = Clause.freshVars cl value
[all...] |
| H A D | Clause.sml | 310 val cl = Clause {parameters = parameters, id = newId (), thm = th} value
[all...] |
| H A D | Proof.sml | 110 val cl = Thm.clause th value
312 val cl = Thm.clause th value
359 val cl = Thm.clause th value
376 val cl = Thm.clause th value
[all...] |
| H A D | Subsume.sml | 262 val cl = clauseSym (LiteralSet.toList cl) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/ |
| H A D | java_raw_api.c | 329 ffi_raw_closure *cl = (ffi_raw_closure*)user_data; local
337 ffi_prep_java_raw_closure_loc (ffi_java_raw_closure* cl, argument
364 ffi_prep_java_raw_closure (ffi_java_raw_closure* cl, argument
[all...] |
| H A D | raw_api.c | 218 ffi_raw_closure *cl = (ffi_raw_closure*)user_data; local
225 ffi_prep_raw_closure_loc (ffi_raw_closure* cl, argument
257 ffi_prep_raw_closure (ffi_raw_closure* cl, argument
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/HolSat/ |
| H A D | minisatParse.sml | 166 val cl = Dynarray.array((Array.length clauseth) * 2,TRUTH) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | selftest.sml | 981 val cl = make_constructorList true [ value
1041 val cl = make_constructorList false [ value
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Proof.C | 83 ClauseId Proof::addRoot(vec<Lit>& cl, ClauseId orig_root_id) argument
|
| /seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
| H A D | hhTranslate.sml | 334 val cl = mk_term_set (List.concat (map (find_cid cid) tml)) value
344 val cl = find_terms is_const cj value
|