Searched refs:Function (Results 1 - 25 of 115) sorted by path

12345

/seL4-l4v-10.1.1/HOL4/Manual/Description/
H A DHolBdd.tex2080 \hbc{failfn : 'a -> 'b}{Function that always raises exception fail (useful as argument to GenTermToTermBdd).}
/seL4-l4v-10.1.1/HOL4/Manual/Interaction/
H A DHOL-interaction.tex233 Function can be defined using {\tt Define}, \eg{} square is defined as follows.
/seL4-l4v-10.1.1/HOL4/Manual/Logic/
H A Dsyntax.tex182 \item {\bf Function types:}\index{function types, in HOL logic@function types, in \HOL{} logic!abstract form of} If $\sigma_1$
357 U}^{n}\longrightarrow{\cal U}$ on the universe. Function types are
525 \item {\bf Function applications:} If $t_{\sigma'{\fun}\sigma}\in{\sf
547 Function application\index{function application, in HOL logic@function application, in \HOL{} logic!associativity of} is assumed to associate
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A DHolBdd.tex2080 \hbc{failfn : 'a -> 'b}{Function that always raises exception fail (useful as argument to GenTermToTermBdd).}
H A Dtactics.tex1871 functions. Function composition occasionally allows a more
/seL4-l4v-10.1.1/HOL4/Manual/Tutorial/
H A Dlogic.tex199 \paragraph{Function application types}
259 \paragraph{Function types}
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/
H A DcoreScript.sml782 (* The State Function ------------------------------------------------------ *)
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A DupdateScript.sml3 (* DESCRIPTION : Function update using lists *)
/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A DCCSLib.sml208 (* Function for applying a list of tactics to a list of subgoals. *)
/seL4-l4v-10.1.1/HOL4/examples/Crypto/TWOFISH/
H A DtwofishScript.sml233 (* Function h takes two inputs--a 32-bit word X and a list L = (L0,...,Lk ) *)
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DDerivedBddRules.sml132 (* Function that always raises exception fail *)
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/
H A DSolitaireScript.sml76 (* Function shuffle below used to create it *)
114 (* Function to create a formula to represent a move in which a counter at v1 *)
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/examples/
H A Dalu.sml3 (* Function makeALU generates HOL term for transition system and init states of sync. pipelined ALU *)
H A Dttt.sml54 (* Function shuffle below used to create it *)
87 (* Function to create a relation to represent a move in which a 'o' or an 'x' *)
/seL4-l4v-10.1.1/HOL4/examples/PSL/regexp/
H A DregexpTools.sml53 (* Function caches. *)
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/
H A DM1Examples.sml31 * Function to simplify imported ACL2
H A Dsexp.sml121 (* Function to add a list of theorems to acl2_simps *)
173 (* Function to add an entry to acl2_names *)
942 (* Function to add a list of string abbreviations to string_abbrevs *)
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dmake_hol_acl2_defaxioms.ml28 (* Function for filtering out definitions - fails on non-definitions *)
H A Dsexp.sml121 (* Function to add a list of theorems to acl2_simps *)
173 (* Function to add an entry to acl2_names *)
868 (* Function to add a list of string abbreviations to string_abbrevs *)
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DencodeLib.sml646 ("Function clause: " ^ term_to_string fname ^
H A DfunctionEncodeLib.sml1664 ("Function to find constructed terms returned a term with a non-compound type: " ^
2853 "Function is not of the form: \"|- !a b. P ==> f a b ... = \"";
H A DpolytypicLib.sig123 (* Function splitting *)
154 (* Function retrieval *)
196 (* Function creation tools *)
H A DpolytypicLib.sml1030 val func_exn = mkDebugExn "SPLIT_HFUN_CONV" "HO Function supplied is of the form \"(f x = A x) /\\ (g x =...\"";
1043 val _ = assert' [("Function list is not a list of variables",all is_var)] fvs
1429 val exn1 = debug_exn "Function clauses are not all of the form \"!x x0 .. xn. f x = A x0 ... xn\""
1481 [("Function term is mutually recursive on different types",
1840 "Function term missing from existence proof")
2412 (* Function generators: *)
3459 (* Function generators *)
H A Dsexp.sml121 (* Function to add a list of theorems to acl2_simps *)
173 (* Function to add an entry to acl2_names *)
868 (* Function to add a list of string abbreviations to string_abbrevs *)
H A DtestACL2encoding.ml126 (* Function testing: *)

Completed in 240 milliseconds

12345