Searched defs:wrap (Results 1 - 21 of 21) sorted by relevance

/seL4-l4v-10.1.1/HOL4/src/parse/
H A DPretype.sml220 val wrap = value
/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A DCCSLib.sig20 val wrap : 'a -> 'a list value
H A DCCSLib.sml43 fun wrap a = [a]; (* from util_prob *) function
/seL4-l4v-10.1.1/HOL4/src/probability/
H A Dutil_probScript.sml32 fun wrap a = [a]; function
H A DlebesgueScript.sml46 fun wrap a = [a]; function
H A DprobabilityScript.sml36 fun wrap a = [a]; function
H A DmeasureScript.sml45 fun wrap a = [a]; function
[all...]
H A Dreal_topologyScript.sml63 fun wrap a = [a]; function
[all...]
/seL4-l4v-10.1.1/HOL4/src/real/
H A DseqScript.sml46 fun wrap a = [a]; function
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/
H A DDEBUGGER_.sml86 fun wrap (f:'a -> unit) (x: 'a) : unit = function
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/
H A DformalizeUseful.sig107 val wrap : 'a -> 'a list value
H A DsubtypeUseful.sig107 val wrap : 'a -> 'a list value
H A DformalizeUseful.sml223 fun wrap a = [a]; function
H A DsubtypeUseful.sml223 fun wrap a = [a]; function
/seL4-l4v-10.1.1/HOL4/examples/miller/useful/
H A DHurdUseful.sig106 val wrap : 'a -> 'a list value
H A DHurdUseful.sml199 fun wrap a = [a]; function
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DCODEGEN_PARSETREE.sml839 val wrap = value
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DencodeLib.sml914 fun wrap e = wrapException "mk_encode_decode_map_conc" e function
1062 fun wrap e = wrapException "mk_encode_decode_conc" e function
1085 fun wrap e = wrapException "mk_decode_encode_conc" e function
1112 fun wrap e = wrapException "mk_encode_detect_conc" e function
1288 let fun wrap e = wrap_full "FULL_FIX_ID_THM" t e function
1331 let fun wrap e = wrap_full "FULL_ENCODE_DECODE_THM" t e function
1378 fun wrap e = wrapException "FULL_DECODE_ENCODE_THM" e function
1419 fun wrap e = wrapException "FULL_ENCODE_DETECT_THM" e function
[all...]
H A DfunctionEncodeLib.sml259 fun wrap e = wrapException "conditionize_rewrite" e function
1769 fun wrap s = wrapException ("clause_to_case_list" ^ s) function
1850 fun wrap e = wrapException "mk_func_case_thm" e function
1892 fun wrap e = wrapException "general_lambda" e function
1909 fun wrap e = wrapException "general_lambda_propagation_term" e function
2025 fun wrap e = wrapException "mk_affirmation_theorems" e function
2351 fun wrap e = wrapException "mk_case_propagation_theorem" e function
3373 fun wrap e = (remove () ; wrapException "encode_until_recursive" e) function
3626 let fun wrap e = wrapException "create_abstract_recognizers" e function
[all...]
H A DpolytypicLib.sml1032 fun wrap e = wrapException "SPLIT_HFUN_CONV" e function
1079 fun wrap UNCHANGED = raise UNCHANGED | wrap e = wrapException "SPLIT_PAIR_CONV" e function
1145 fun wrap e = wrapException "SPLIT_FUNCTION_CONV" e function
1290 fun wrap "" e = wrapException "create_mutual_theorem" e function
1433 fun wrap "" e = wrapException "instantiate_mutual_theorem" e function
1530 fun wrap e = wrapException "create_ind_theorem" e function
1673 fun wrap e = wrapException "prove_induction_recursion_thms" e; function
2778 fun wrap "" e = wrapException ("expanded_function_def") e function
2856 let fun wrap e = wrapException ("mk_split_" ^ func ^ "_function (mk_eq_thm)") e function
2931 fun wrap "" e = wrapException "strengthenProof" e function
3008 fun wrap e = wrapException "prove_split_term" e function
3133 fun wrap "" e = wrapException "prove_all_split_terms" e function
3209 fun wrap "" e = wrapException "remove_hyp_terms" e function
3304 fun wrap e = wrapException "unsplit_function" e function
3411 fun wrap e = wrapException "mk_source_functions" e function
3424 fun wrap e = wrapException "mk_coding_functions" e function
3441 fun wrap e = wrapException "mk_target_functions" e function
[all...]
/seL4-l4v-10.1.1/HOL4/src/list/src/
H A DlistScript.sml3809 fun wrap a = [a]; (* from util_prob *) function

Completed in 254 milliseconds