| /seL4-l4v-master/HOL4/Manual/Logic/ |
| H A D | syntax.tex | [all...] |
| /seL4-l4v-master/HOL4/src/postkernel/ |
| H A D | TheoryReader.sml | 31 val terms = map (Term.read_raw tmvector) encoded_hypscon value
|
| H A D | SharingTables.sml | 481 val terms = map (Term.read_raw tmvector) encoded_hypscon value
|
| H A D | Theory.sml | [all...] |
| /seL4-l4v-master/HOL4/src/rational/ |
| H A D | schneiderUtils.sml | 250 val terms = map (fn (asm,g) =>if null asm then g value
|
| /seL4-l4v-master/HOL4/tools/mlyacc/mlyacclib/ |
| H A D | MLY_base-sig.sml | 245 val terms: LrTable.term list value
|
| /seL4-l4v-master/HOL4/examples/RL_Environment/ |
| H A D | RL_Actions.sml | 401 let val terms = RL_Goal_manager.terms_of_current_goal goal_state value
|
| /seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
| H A D | getting.tex | [all...] |
| /seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
| H A D | base.sig | 221 val terms: LrTable.term list value
|
| /seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
| H A D | getting.tex | [all...] |
| /seL4-l4v-master/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
| H A D | base.sig | 221 val terms: LrTable.term list value
|
| /seL4-l4v-master/HOL4/Manual/Description/ |
| H A D | misc.tex | [all...] |
| H A D | HolBdd.tex | [all...] |
| /seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
| H A D | HolBdd.tex | [all...] |
| /seL4-l4v-master/HOL4/tools/mlyacc/src/ |
| H A D | yacc-grm.sml | 392 val terms = (T 0) :: (T 1) :: (T 2) :: (T 3) :: (T 4) :: (T 5) :: (T 6 value
|
| H A D | yacc.sml | 851 val terms = let fun f n = if n=numTerms then nil value
[all...] |
| /seL4-l4v-master/HOL4/examples/acl2/ml/ |
| H A D | acl2encodeLib.sml | 1199 val terms = if is_fmap t then [combinSyntax.mk_o(valOf enc, encodeLib.get_decode_function target (fdom t)), value
|
| H A D | functionEncodeLib.sml | 237 val terms = find_terms (fn x => (curry op= a' o rator) x handle _ => false) (concl thm') value
273 val terms = terms1; value
1188 let val (terms,disjs) = (map strip_conj ## strip_disj) (strip_imp_only conj) value
1292 val terms = strip_conj (fst (dest_imp_only (concl thm))) value
1660 val terms = map (fn y => (repeat rator (om (concl y)),y)) clauses value
1894 let val terms = map (length o strip_pair) (fst (strip_pabs tm)) value
2042 val terms = hyp negated value
3218 val terms = map (fst o strip_comb o lhs o snd o strip_imp o value
3639 val (terms,r) = encode_until_recursive [f o rand] ([],general_detects) value
[all...] |
| H A D | polytypicLib.sml | 1746 val terms = strip_conj ante value
2859 val terms = map (mk_term o fst) recursive_types handle e => wrap e value
3060 let val terms = find_terms (fn t => (exists (curry op= (rator t) o snd o snd) equivs handle _ => false)) value
3085 val terms = (strip_conj o fst o dest_imp_only o concl) inst handle e => wrap e value
3171 val terms = filter is_imp_only (hyp thm) value
[all...] |
| /seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
| H A D | Term.sml | 716 val terms = everything (termParser >> singleton) tokens value
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Term.sml | 716 val terms = everything (termParser >> singleton) tokens value
|
| /seL4-l4v-master/l4v/tools/c-parser/tools/mlyacc/src/ |
| H A D | yacc-grm.sml | 393 val terms = (T 0) :: (T 1) :: (T 2) :: (T 3) :: (T 4) :: (T 5) :: (T 6 value
|
| /seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
| H A D | helperLib.sml | 634 fun terms ([],x) = ((hd (filter frame_var xs),x) handle Empty => (list_mk_star [] (type_of (car tm1)),x)) function
1290 fun terms ([],x) = ((hd (filter frame_var xs),x) handle Empty => (list_mk_star [] (type_of (car tm1)),x)) function
[all...] |