Lines Matching refs:context
187 simplifier is available, which allows to use context
192 - using context information
222 3: context -> conversion
224 thm list -> (*context that might be used*)
239 context : thm list
240 A list of theorems from the context it may use.
260 new context information that may be assumed theorems are build
265 the old context theorems that can be used
293 different levels of using context information. If more
294 context is used, potentially more can be done. However,
297 different levels of using context information.
302 (* do not use context at all *)
308 (* use all available context (from and, or, ...) *)
376 3: context -> conversion
378 thm list -> (*context that might be used*)
381 (* Use congruences for given context level and argument consequence consequence conv
382 might use context. *)
413 thm list -> (* context *)