| /seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
| H A D | tttInfix.sml | 93 val l0 = String.tokens Char.isSpace value
|
| H A D | tttThmData.sml | 31 val l0 = readl (ttt_thmfea_dir ^ "/" ^ thy) value
73 val l0 = filter in_curthy (dlist (!ttt_thmfea)) value
|
| H A D | tttExec.sml | 100 val l0 = #allVal (PolyML.globalNameSpace) () value
110 val l0 = #allVal (PolyML.globalNameSpace) () value
|
| H A D | tttTermData.sml | 183 let val l0 = tttLexer.ttt_lex (String.concatWith " " (readl file)) in value
|
| H A D | tacticToe.sml | 95 val l0 = debug_t "thmknn_wdep" value
117 val l0 = debug_t "stacknn" value
|
| H A D | tttPredict.sml | 90 val l0 = map f feal value
216 let val l0 = thmknn (symweight,feav) n gfea in value
266 val l0 = List.concat (map (rev o find_terms not_term) (w :: asl)) value
|
| H A D | tttTacticData.sml | 245 val (l0,cont0) = readcat_list m value
271 val l0 = tttLexer.ttt_lex (String.concatWith " " (readl file)) value
|
| H A D | tttSynt.sml | 164 val l0 = List.concat (map f tml) value
250 val l0 = dlist patceptdict value
264 val l0 = dlist ceptpatdict value
515 val l0 = map snd (dlist genthmdict) value
|
| H A D | tttSearch.sml | 564 val l0 = self_selsc :: List.map f (!children) value
812 val l0 = filter (fn x => is_active (fst x)) (dlist (!proofdict)) value
|
| H A D | tttTools.sml | 88 val l0 = all_files dir value
|
| H A D | tttUnfold.sml | 693 val l0 = String.tokens (fn x => x = #".") s value
1227 val l0 = sigobj_theories () value
|
| /seL4-l4v-10.1.1/HOL4/src/compute/examples/ |
| H A D | MergeSort.sml | 78 val l0 = --`[] : num list`--; value
|
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | TheoryReader.sml | 245 val (l0,cont) = read_list m value
270 val l0 = H "read_thydata" read_thydata path value
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Rewrite.sml | 498 val (l0,r0) = eq0 value
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Rewrite.sml | 498 val (l0,r0) = eq0 value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Pmatch.sml | 316 val (l0, l1) = Lib.split_after n l value
322 val (l0, l1) = Lib.split_after n l' value
|
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | constrFamiliesLib.sml | 332 val l0 = variant [r0] r0 value
|
| /seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
| H A D | Induction.sml | 143 val (l0, l1) = Lib.split_after n l value
149 val (l0, l1) = Lib.split_after n l' value
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootParser.sml | 851 val l0 = map (holfoot_p_statement2absyn funL resL gv vs) stmL; value
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/ |
| H A D | ind_types.sml | 1089 val (l0,r0) = dest_eq tm0 value
|