Searched defs:mk_eq (Results 1 - 16 of 16) sorted by relevance
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | Psyntax.sml | 17 val mk_eq = boolSyntax.mk_eq value
|
| H A D | Psyntax.sig | 16 val mk_eq : term * term -> term value
|
| H A D | Rsyntax.sig | 16 val mk_eq : {lhs:term, rhs:term} -> term value
|
| H A D | Rsyntax.sml | 15 fun mk_eq{lhs,rhs} = boolSyntax.mk_eq(lhs,rhs) function
|
| H A D | boolSyntax.sig | 38 val mk_eq : term * term -> term value
|
| H A D | boolSyntax.sml | 48 fun mk_eq (lhs, rhs) = function
|
| /seL4-l4v-master/HOL4/src/ring/src/ |
| H A D | ringLib.sml | 190 fun mk_eq th1 th2 = function
229 val mk_eq = binop_eq Ty value
|
| /seL4-l4v-master/HOL4/src/parse/ |
| H A D | Absyn.sig | 25 val mk_eq : absyn * absyn -> absyn value
|
| H A D | Absyn.sml | 175 val mk_eq = mk_binop "=" value
|
| H A D | Preterm.sml | 735 fun mk_eq(t1, t2) = let function
|
| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | mlibTerm.sig | 101 val mk_eq : term * term -> formula value
|
| H A D | mlibTerm.sml | 565 fun mk_eq (a, b) = Atom (Fn ("=", [a, b])); function
|
| /seL4-l4v-master/graph-refine/ |
| H A D | stack_logic.py | 20 from syntax import mk_var, word32T, builtinTs, mk_eq, mk_less_eq namespace
878 from syntax import mk_eq, mk_implies, mk_var namespace
|
| H A D | syntax.py | 1349 def mk_eq (x, y): function
|
| /seL4-l4v-master/HOL4/src/postkernel/ |
| H A D | Theory.sml | 1154 fun mk_eq (lhs,rhs) = function
|
| /seL4-l4v-master/HOL4/src/bool/ |
| H A D | boolScript.sml | 355 fun mk_eq(lhs,rhs) = ���^lhs = ^rhs���; function
3759 fun mk_eq th = function
[all...] |
Completed in 110 milliseconds