| /seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
| H A D | CODETREE_SIMPLIFIER.sml | 133 compiler was compiled on. The ML word length will be the same because
1626 (* Frequently we will have produced an indirection from the same base. These
1640 (* It has to be the same base and with increasing offsets
|
| H A D | CODETREE_OPTIMISER.sml | 325 (* Each argument list should be the same length.
507 has the same calling pattern as the original. This simply
|
| /seL4-l4v-master/HOL4/src/probability/ |
| H A D | measureScript.sml | 1193 (* added the same more requirements as for MEASURE_PRESERVING_LIFT *)
2429 RW_TAC std_ss [] \\ (* 3 subgoals, same tactics *)
3578 >- (GEN_TAC >> DISCH_TAC >> CONJ_TAC \\ (* 2 subgoals, same tactics *)
3592 >- (GEN_TAC >> DISCH_TAC >> CONJ_TAC \\ (* 2 subgoals, same tactics *)
3666 >- (rpt STRIP_TAC \\ (* 3 subgoals, same tactics *)
4266 RW_TAC std_ss [SUBSET_DEF, IN_POW, IN_BIGUNION] \\ (* 2 subgoals, same tactics *)
|
| /seL4-l4v-master/HOL4/src/pred_set/src/ |
| H A D | pred_setScript.sml | 383 same pattern to "" *)
2201 >- ( BasicProvers.NORM_TAC std_ss [INJ_DEF] \\ (* 2 sub-goals, same tactical *)
3217 EXISTS_UNIQUE_ALT] \\ (* 2 sub-goals here, same tacticals *)
4643 This constant is the same as standard mathematics \Sigma operator:
4918 val _ = set_fixity "PERMUTES" (Infix(NONASSOC, 450)); (* same as relation *)
5004 This construct is the same as standard mathematics \Pi operator:
|
| /seL4-l4v-master/HOL4/Manual/Description/ |
| H A D | version2.tex | 260 search path has precisely the same format as the regular search path,
943 \ml{ |- (\(n\)=\(m\)) = T }if \(n\) and \(m\) represent the same number,\\
|
| /seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
| H A D | version2.tex | 260 search path has precisely the same format as the regular search path,
943 \ml{ |- (\(n\)=\(m\)) = T }if \(n\) and \(m\) represent the same number,\\
|
| /seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/ |
| H A D | combin.tex | 819 We do exactly the same thing for the reflexive and transitive closure
850 \label{sec:Proving-RTCs-same}
|
| /seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
| H A D | user_lemma_primitive_operationsScript.sml | 657 (* received same value in Lookup *)
734 (* received same value in Lookup *)
|
| /seL4-l4v-master/HOL4/examples/HolCheck/ |
| H A D | lzPairRules.sml | 268 (* v is a term of the same type as tuple p; return a list of substs in which components of p are matched to v via FST and SND *)
2101 (* Paired stripping tactics, same as basic ones, but they use PGEN_TAC *)
|
| /seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
| H A D | advanced.tex | 849 in the context of a particular subgoal: free variables receive the same
968 res_inst_tac}. At the same time, we shall have a glimpse at Isabelle's
|
| /seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
| H A D | advanced.tex | 849 in the context of a particular subgoal: free variables receive the same
968 res_inst_tac}. At the same time, we shall have a glimpse at Isabelle's
|
| /seL4-l4v-master/HOL4/src/emit/ |
| H A D | EmitML.sml | 98 (* we want the resulting ML to look the same, i.e., be readable, no matter *)
209 (* C' is a variable with the same name as C. This code only deals with *)
|
| /seL4-l4v-master/HOL4/examples/CCS/ |
| H A D | ContractionScript.sml | 54 (* the proof is the same with EXPANSION_EPS *)
1779 >| [ (* goal 1 (of 2), same as goal 2 of COARSEST_CONGR_RL *)
|
| /seL4-l4v-master/HOL4/examples/algebra/group/ |
| H A D | finiteGroupScript.sml | 704 (3) d IN s1 /\ d IN s2 ==> (left z * d,|/ d * mright z) IN preimage f s z, same as (1).
919 (* Another proof of the same theorem *)
|
| /seL4-l4v-master/HOL4/examples/algebra/ring/ |
| H A D | quotientRingScript.sml | 930 (2) same as (1)
941 (4) same as (1)
|
| /seL4-l4v-master/isabelle/src/Pure/PIDE/ |
| H A D | document.scala | 333 perspective.visible.same(other_perspective.visible) &&
|
| /seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/ |
| H A D | document.scala | 333 perspective.visible.same(other_perspective.visible) &&
|
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | Pmatch.sml | 439 (* If all cases lead to the same result, no split is necessary *)
|
| /seL4-l4v-master/HOL4/src/datatype/mutrec/ |
| H A D | Recftn.sml | 21 Both examples define the same functions, a set of functions that
|
| /seL4-l4v-master/HOL4/src/finite_maps/ |
| H A D | fmapalTacs.sml | 163 (* and FMAPAL terms. enumTacs has the same for OWL and ENUMERAL. *)
|
| /seL4-l4v-master/HOL4/src/floating-point/ |
| H A D | binary_ieeeLib.sml | 743 The latter two cases only apply when either ``a`` or ``b`` is the same
|
| /seL4-l4v-master/HOL4/src/integer/ |
| H A D | CooperShell.sml | 546 if two divisibility constraints exist with the same set of free
|
| /seL4-l4v-master/HOL4/src/pattern_matches/ |
| H A D | patternMatchesScript.sml | 554 same value. I will call such rows subsumed. *)
|
| /seL4-l4v-master/HOL4/src/quotient/examples/lambda/ |
| H A D | etaScript.sml | 223 (* change the term, then either the variables were the same, or *)
|
| /seL4-l4v-master/HOL4/tools/mlyacc/src/ |
| H A D | yacc.sml | 682 terminals associated with that precedence. The list has the same order as
|