/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibMatch.sig | 11 type subst = mlibSubst.subst type 14 val matchl : subst -> (term * term) list -> subst 15 val match : term -> term -> subst 16 val matchl_literals : subst -> (formula * formula) list -> subst 17 val match_literals : formula -> formula -> subst 20 val unifyl : subst -> (term * term) list -> subst [all...] |
H A D | mlibSubst.sig | 14 type subst type 16 val |<>| : subst 17 val ::> : (string, term) maplet * subst -> subst 18 val @> : subst * subst -> subst 19 val null : subst -> bool 20 val term_subst : subst -> term -> term 21 val formula_subst : subst [all...] |
H A D | mlibSubsume.sig | 13 type subst = mlibSubst.subst type 24 val subsumes : 'a subsume -> formula list -> (subst * 'a) stream 27 val subsumes' : 'a subsume -> formula list -> (subst * 'a) stream 30 val subsumes1 : formula list -> formula list -> subst list 31 val subsumes1' : formula list -> formula list -> subst list
|
H A D | mlibKernel.sig | 11 type subst = mlibSubst.subst type 24 val INST : subst -> thm -> thm
|
H A D | mlibTermorder.sig | 11 type subst = mlibSubst.subst type 30 val subst : subst -> termorder -> termorder value
|
H A D | matchTools.sig | 9 type ('a, 'b) subst = ('a, 'b) Lib.subst 13 type tySubst = (hol_type, hol_type) subst 14 type Subst = (term, term) subst * tySubst
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Subst.sig | 13 type subst type 19 val empty : subst 21 val null : subst -> bool 23 val size : subst -> int 25 val peek : subst -> Term.var -> Term.term option 27 val insert : subst -> Term.var * Term.term -> subst 29 val singleton : Term.var * Term.term -> subst 31 val toList : subst -> (Term.var * Term.term) list 33 val fromList : (Term.var * Term.term) list -> subst 53 val subst : subst -> Term.term -> Term.term value [all...] |
H A D | Subsume.sig | 32 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> 33 (Thm.clause * Subst.subst * 'a) option 38 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> 39 (Thm.clause * Subst.subst * 'a) option 47 val clauseSubsumes : Thm.clause -> Thm.clause -> Subst.subst option 49 val clauseStrictlySubsumes : Thm.clause -> Thm.clause -> Subst.subst option
|
H A D | Atom.sig | 81 val subst : Subst.subst -> atom -> atom value 87 val match : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *) 93 val unify : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Subst.sig | 13 type subst type 19 val empty : subst 21 val null : subst -> bool 23 val size : subst -> int 25 val peek : subst -> Term.var -> Term.term option 27 val insert : subst -> Term.var * Term.term -> subst 29 val singleton : Term.var * Term.term -> subst 31 val toList : subst -> (Term.var * Term.term) list 33 val fromList : (Term.var * Term.term) list -> subst 53 val subst : subst -> Term.term -> Term.term value [all...] |
H A D | Subsume.sig | 32 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> 33 (Thm.clause * Subst.subst * 'a) option 38 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> 39 (Thm.clause * Subst.subst * 'a) option 47 val clauseSubsumes : Thm.clause -> Thm.clause -> Subst.subst option 49 val clauseStrictlySubsumes : Thm.clause -> Thm.clause -> Subst.subst option
|
H A D | Atom.sig | 81 val subst : Subst.subst -> atom -> atom value 87 val match : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *) 93 val unify : Subst.subst -> atom -> atom -> Subst.subst (* raises Error *)
|
/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/ |
H A D | commonUnifScript.sml | 12 `!subst source z. 14 (!m n. m < n ==> (subst m) SUBMAP (subst n)) /\ 15 (!n. DISJOINT (FDOM (subst n)) (source n)) /\ 16 (!n. z < n ==> (FDOM (subst n) UNION (source n) = FDOM (subst z) UNION (source z)))) 17 ==> ?x. !n. x < n ==> ((subst n) = (subst x)))`, 32 `?n.m < n /\ subst m <> subst [all...] |
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/ |
H A D | Cond_rewrite.sig | 15 :(term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list) 19 :term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list 21 :(term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list)
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Unify.sig | 13 term list -> term -> term -> (term,term)subst -> (term,term)subst 14 val simp_unify_terms : term list -> term -> term -> (term,term)subst 18 val deref_tmenv : (term,term)subst -> term -> term 22 val restrict_tmenv :(term -> bool) -> (term,term)subst -> (term,term)subst
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | stringfindreplace.sig | 4 val subst : {redex:string,residue:string} list -> string -> string value
|
H A D | FinalType-sig.sml | 39 val type_subst : (hol_type,hol_type) Lib.subst -> hol_type -> hol_type 41 val match_type : hol_type -> hol_type -> (hol_type,hol_type) Lib.subst 44 -> (hol_type,hol_type) Lib.subst 47 -> (hol_type,hol_type)Lib.subst 48 -> (hol_type,hol_type)Lib.subst 50 -> (hol_type,hol_type) Lib.subst * hol_type list 51 -> (hol_type,hol_type) Lib.subst * hol_type list 55 val ty_sub : (hol_type,hol_type) Lib.subst -> hol_type ->
|
H A D | FinalTerm-sig.sml | 6 type ('a,'b)subst = ('a,'b)Lib.subst 64 val subst : (term,term) subst -> term -> term value 65 val inst : (hol_type,hol_type) subst -> term -> term 69 -> (term,term)subst * (hol_type,hol_type)subst 70 -> ((term,term)subst * term set) * 71 ((hol_type,hol_type)subst * hol_type list) 73 -> (term,term)subst * (hol_typ [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
H A D | armLib.sig | 14 val RES_MP1_TAC : (term frag list, term frag list) subst -> thm -> tactic 15 val RES_MP_TAC : (term frag list, term frag list) subst -> thm -> tactic
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | armLib.sig | 12 val RES_MP1_TAC : (term frag list, term frag list) subst -> thm -> tactic 13 val RES_MP_TAC : (term frag list, term frag list) subst -> thm -> tactic
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Rules.sig | 3 type ('a,'b) subst = ('a,'b)Lib.subst 14 val IT_EXISTS : (term,term) subst -> thm -> thm
|
H A D | wfrecUtils.sig | 25 val match_type : 'a -> hol_type -> hol_type -> (hol_type,hol_type)subst 27 -> (term,term) subst * (hol_type,hol_type) subst
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Abbrev.sml | 17 type ('a,'b)subst = ('a,'b) Lib.subst
|
H A D | Abbrev.sig | 19 type ('a,'b)subst = ('a,'b) Lib.subst
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/utils/ |
H A D | elsaUtils.sig | 43 val STRONG_INST :{term_substitution:(term,term)Lib.subst, theorem:thm} -> thm 45 :{theorem:thm,type_substitution:(hol_type,hol_type) Lib.subst} -> thm 46 val STRONG_INST_TY_TERM :{term_substitution:(term,term) Lib.subst, 48 type_substitution:(hol_type,hol_type)Lib.subst} -> 53 -> (term,term) Lib.subst * (hol_type,hol_type) Lib.subst
|