| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/ |
| H A D | termScript.sml | 599 (* object, dict, entry, or method substitution operators defined: *)
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
| H A D | numerics.tex | 27 Isabelle's arithmetic decision procedure, the method
247 The \isa{arith} method can prove facts about \isa{abs} automatically,
|
| H A D | sets.tex | 571 This can be proved using the \isa{auto} method.
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
| H A D | numerics.tex | 27 Isabelle's arithmetic decision procedure, the method
247 The \isa{arith} method can prove facts about \isa{abs} automatically,
|
| H A D | sets.tex | 571 This can be proved using the \isa{auto} method.
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
| H A D | document_model.scala | 643 Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
| H A D | document_model.scala | 643 Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
|
| /seL4-l4v-10.1.1/HOL4/src/holyhammer/legacy/ |
| H A D | hh_tac.ml | 219 escaping method'word')
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
| H A D | alphaScript.sml | 40 (* Define semantics for objects, methods, and method dictionaries. *)
54 (* method ::= sigma(x)b *)
2339 (* It has two forms, one for method invocation and one for update. *)
2356 (* Definition of method invocation. *)
|
| /seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/ |
| H A D | description.tex | 117 The syntax for restricted quantification provides a method of
|
| /seL4-l4v-10.1.1/HOL4/tools/mlyacc/mlyacclib/ |
| H A D | MLY_parser2.sml | 42 This program is an implementation is the partial, deferred method discussed
|
| /seL4-l4v-10.1.1/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
| H A D | parser2.sml | 12 This program is an implementation is the partial, deferred method discussed
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
| H A D | parser2.sml | 12 This program is an implementation is the partial, deferred method discussed
|
| /seL4-l4v-10.1.1/HOL4/src/IndDef/Manual/ |
| H A D | paper.tex | 50 approach, as opposed to the axiomatic method, is that each of the primitive
225 Using this method of expressing the notion of \mbox{closure} under a set of
|
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | version2.tex | 78 {\small\verb%!%}, {\small\verb%?%} and {\small\verb%@%}. This provides a method of
272 Meeting and implements a method of simulating subtypes and dependent
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | version2.tex | 78 {\small\verb%!%}, {\small\verb%?%} and {\small\verb%@%}. This provides a method of
272 Meeting and implements a method of simulating subtypes and dependent
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Tactic.sml | 4 (* method due to Robin Milner. This file has been *)
|
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | patternMatchesScript.sml | 259 use this method to construct the desired correspondance. *)
|
| /seL4-l4v-10.1.1/HOL4/Manual/Logic/ |
| H A D | semantics.tex | 1043 \equant{x_\sigma}t'$ and one can apply the method of constant
1070 example given in that Remark is not so much the method of extension by
|
| /seL4-l4v-10.1.1/HOL4/src/enumfset/ |
| H A D | enumeralScript.sml | 431 (* comparisons of the general method. (See better_bt_to_ol below.) *)
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractLib.sml | 204 plan: provide a method which, given a list of definition and
|
| /seL4-l4v-10.1.1/HOL4/examples/CCS/ |
| H A D | CongruenceScript.sml | 395 (* The congruence built by above method is the coarsest congruence contained in R *)
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Logics_ZF/document/ |
| H A D | ZF.tex | 1393 conditional rewrite rules. Call the method \ttindex{typecheck} to
1790 % we also have the ind_cases method, but what does it do?
1888 An alternative proof uses Isar's fancy \isa{induct} method, which
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics_ZF/document/ |
| H A D | ZF.tex | 1393 conditional rewrite rules. Call the method \ttindex{typecheck} to
1790 % we also have the ind_cases method, but what does it do?
1888 An alternative proof uses Isar's fancy \isa{induct} method, which
|
| /seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/doc/ |
| H A D | ds.tex | 714 equivalence instead of just an implication. A similar method is used by newer
|