| /seL4-l4v-10.1.1/HOL4/src/datatype/theory_tests/ |
| H A D | ndatatype_ind0Script.sml | 32 fun check (tac, t) = (tac([], t) before ignore (save_thm( function
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/lisp/ |
| H A D | check-file.lisp | [all...] |
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | selftest.sml | 167 fun check (Exn.Res th) = rhs (concl th) ~~ T function
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | base_tokens.sml | 21 fun check p exnstring (s,loc) = let function
23 fun check ss = function
|
| H A D | testutils.sml | 186 fun check res = function
201 fun check (Res r) = false function
|
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | Int32.sml | 34 fun check i = function
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibModel.sig | 45 val check : model -> formula -> bool value
|
| H A D | mlibUnits.sml | 52 fun check t = (unify_literals |<>| (dest_unit t) lit, t) function
|
| H A D | mlibSubst.sml | 102 fun check (a, b, (c, d)) = function
|
| H A D | mlibResolution.sml | 152 and check set sos n (d,cl) = function
|
| /seL4-l4v-10.1.1/HOL4/src/pred_set/src/ |
| H A D | PSet_ind.sml | 34 local val check = assert (fn tm => value
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Units.sml | 58 fun check (uTh as (lit',_)) = function
|
| H A D | PortableMosml.sml | 140 fun check i = String.substring (s,i,sizeP) = p function
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Units.sml | 58 fun check (uTh as (lit',_)) = function
|
| H A D | PortableMosml.sml | 140 fun check i = String.substring (s,i,sizeP) = p function
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/ |
| H A D | UTF8.sml | 117 and check acc pos start cnt = value
|
| /seL4-l4v-10.1.1/HOL4/src/simp/src/ |
| H A D | selftest.sml | 98 fun check (th1, th2) = function
115 fun check th = aconv (rhs (concl th)) ``f (x:'a):'a = z`` function
130 fun check th = not (aconv (rhs (concl th)) ``x:bool``) function
145 fun check th = aconv (rhs (concl th)) result function
156 fun check th = aconv (rhs (concl th)) result function
167 fun check th = aconv (rhs (concl th)) result function
181 fun check (sgs, vfn) = let function
200 fun check th = th |> concl |> rhs |> aconv F function
210 fun check th = th |> concl |> rhs |> aconv F function
[all...] |
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | inst_logic.py | 15 import check namespace
|
| H A D | stats.py | 8 import check namespace
|
| /seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
| H A D | regexp2dfa.sml | 327 fun check(J,lstring,name,string) = function
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/ |
| H A D | m0AssemblerLib.sml | 126 fun check (add, label, line) x ast = function
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Thm_cont.sml | 394 fun check ex [] = raise ex function
|
| /seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
| H A D | QbfCertificate.sml | 178 fun check t dict (VALID (exts,lits)) = let function
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Main.C | 205 bool check = false; local
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | intSimps.sml | 251 fun check tm = function
|