/seL4-l4v-10.1.1/isabelle/Admin/lib/Tools/ |
H A D | makedist | 95 IDENT=$("$HG" --repository "$ISABELLE_HOME" id -r "$VERSION" -i) 96 [ -z "$IDENT" ] && fail "Bad repository version: \"$VERSION\"" 108 DISTVERSION="Isabelle repository snapshot $IDENT $DATE" 128 "$HG" --repository "$ISABELLE_HOME" archive --type files -r "$IDENT" "$DIR" || \ 150 echo "This is a snapshot of Isabelle/${IDENT} from the repository." 166 perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings 218 echo "$IDENT" > "$DISTPREFIX/ISABELLE_IDENT"
|
/seL4-l4v-10.1.1/l4v/isabelle/Admin/lib/Tools/ |
H A D | makedist | 95 IDENT=$("$HG" --repository "$ISABELLE_HOME" id -r "$VERSION" -i) 96 [ -z "$IDENT" ] && fail "Bad repository version: \"$VERSION\"" 108 DISTVERSION="Isabelle repository snapshot $IDENT $DATE" 128 "$HG" --repository "$ISABELLE_HOME" archive --type files -r "$IDENT" "$DIR" || \ 150 echo "This is a snapshot of Isabelle/${IDENT} from the repository." 166 perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings 218 echo "$IDENT" > "$DISTPREFIX/ISABELLE_IDENT"
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Absyn_dtype.sml | 12 | IDENT of locn.locn * string
|
H A D | Absyn.sml | 30 fun ultimately s (IDENT (_, s')) = (s = s') 37 | IDENT (locn,_) => locn 57 | IDENT p => VIDENT p 96 fun mk_ident s = IDENT(nolocn,s) 107 fun dest_ident (IDENT (_,s)) = s 162 fun dest (APP(_,APP(_,IDENT (locn,s),M),N)) = if s=str then (M,N) else raise err locn 226 fun dest (APP(_,IDENT (locn,s),M)) = if s=str then dest_lam M else raise err locn
|
H A D | TermParse.sml | 113 IDENT(l, nm) => term_grammar.preterm_processor TmG (nm, length args) 122 APP(l,APP(_,IDENT (_,"gspec special"), t1), t2) => 124 | APP(l,APP(_,APP(_,IDENT (_, "gspec2 special"), t1), t2), t3) => 132 | APP(l, APP(_, t0 as IDENT (_, caseform), t1), t2) => 155 APP(l, APP(_, t0 as IDENT (_, casearrow), t1), t2) => 176 | APP (l1, APP (l2, IDENT (l3, fupd), t1), r) => 203 | IDENT (l, s) => make_atom oinfo l s
|
/seL4-l4v-10.1.1/HOL4/src/monad/ |
H A D | parmonadsyntax.sml | 44 | IDENT x => VIDENT x 48 | APP(loc1, APP(loc2, IDENT (loc3, ","), arg1), arg2) => 65 APP(loc1, APP(loc2, IDENT(loc3, s), arg1), arg2) => let 74 APP(loc1, APP(loc2, IDENT(loc3, s), a1), a2)) 85 APP(loc1, APP(loc2, IDENT(loc3, s), arg1), arg2) => let 96 IDENT(loc3, monad_bind), 114 APP(l,arg1 as APP(_,IDENT(_,s),_),arg2) => 121 | IDENT(loc,s) => if s = monad_emptyseq_special then 137 IDENT(loc,s) => if s = monad_emptyseq_special then NONE
|
H A D | monadsyntax.sml | 134 | IDENT x => VIDENT x 138 | APP(loc1, APP(loc2, IDENT (loc3, ","), arg1), arg2) => 149 APP(loc1, APP(loc2, IDENT(loc3, s), arg1), arg2) => let 162 APP(loc1, APP(loc2, IDENT(loc3, s), arg1), arg2) => let 175 IDENT(loc3, monad_unitbind), 180 IDENT(loc3, monad_bind), 198 APP(l,arg1 as APP(_,IDENT(_,s),_),arg2) => 205 | IDENT(loc,s) => if s = monad_emptyseq_special then 221 IDENT(loc,s) => if s = monad_emptyseq_special then NONE
|
/seL4-l4v-10.1.1/HOL4/src/bool/ |
H A D | boolpp.sml | 246 APP(_,APP(_,IDENT(_,andstr),t1),t2) => if andstr = and_special then 262 APP(binding_locn,IDENT (binding_locn,"LET"),b), 270 fun let_remove f (APP(_,APP(_,IDENT _, t1), t2)) = munge_let (f t1) (f t2) 273 traverse (fn APP(_,APP(_,IDENT (_,letstr), _), _) => letstr = let_special 276 traverse (fn IDENT(_,andstr) => andstr = and_special | _ => false) 285 fun nilcheck (APP (_, IDENT (_, nilstr), body)) = nilstr = letnil_special 288 APP (_, IDENT (_, letstr), 290 APP(_, IDENT(_, constr), eq1), 297 APP (l1, APP (l2, IDENT(_, constr), eq1), eqs) => 299 APP (l1, APP (l2, IDENT(l [all...] |
/seL4-l4v-10.1.1/HOL4/src/ring/src/ |
H A D | abs_tools.sml | 14 let fun add_ip (c as IDENT(locn,s)) = foldl (fn (v,pt) => APP(locn,pt,v)) c (impl_of s)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Isar/ |
H A D | parse.scala | 80 tok.kind == Token.Kind.IDENT ||
|
H A D | token.scala | 23 val IDENT = Value("identifier") 77 { case x ~ Nil => Token(Token.Kind.IDENT, x) 278 def is_ident: Boolean = kind == Token.Kind.IDENT 284 kind == Token.Kind.IDENT ||
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Isar/ |
H A D | parse.scala | 80 tok.kind == Token.Kind.IDENT ||
|
H A D | token.scala | 23 val IDENT = Value("identifier") 77 { case x ~ Nil => Token(Token.Kind.IDENT, x) 278 def is_ident: Boolean = kind == Token.Kind.IDENT 284 kind == Token.Kind.IDENT ||
|
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | holindex.lex | 68 handle Binarymap.NotFound => IDENT (mkTok I text pos line);
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | parsePMATCH.sml | 188 APP(l1, APP(l2, IDENT (l3, arr), lh), rh) => 196 APP(_, APP(_, IDENT (_, bvsplit), bvs), body) => 202 APP(_, APP(_, IDENT(_, gdsplit), pat), gd) => 269 APP(l1, APP(l2, IDENT(l3, c), arg1), arg2) =>
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootParser.sml | 72 | Absyn.IDENT (locn,i) => 105 fun col set l s = (Redblackset.add (set,s), Absyn.IDENT (l, s)) 130 (qv', Absyn.IDENT (l, i')) 131 end else (qv, Absyn.IDENT (l, i)) 154 (set, Absyn.mk_AQ (assoc i substL))) handle HOL_ERR _ => (set, Absyn.IDENT (l, i)) 168 | Absyn.IDENT (locn,i) => (os_opt, l) 170 | Absyn.APP (locn,Absyn.IDENT(_,"old"),Absyn.IDENT(_,v)) => 183 (SOME os', Absyn.IDENT (locn,(fst o dest_var) nv)) 223 (set, Absyn.IDENT ( [all...] |
H A D | holfoot.lex | 66 handle Binarymap.NotFound => IDENT (mkTok I text pos line);
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | bibtex.scala | 326 val IDENT = Value("identifier") 338 kind == Token.Kind.IDENT 341 kind == Token.Kind.IDENT 492 private val ident = identifier ^^ token(Token.Kind.IDENT) 518 else Token.Kind.IDENT
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/ |
H A D | bibtex.scala | 326 val IDENT = Value("identifier") 338 kind == Token.Kind.IDENT 341 kind == Token.Kind.IDENT 492 private val ident = identifier ^^ token(Token.Kind.IDENT) 518 else Token.Kind.IDENT
|
/seL4-l4v-10.1.1/isabelle/src/Pure/ML/ |
H A D | ml_lex.scala | 44 val IDENT = Value("identifier") 199 val ident = (alphanumeric | symbolic) ^^ (x => Token(Kind.IDENT, x))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/ML/ |
H A D | ml_lex.scala | 44 val IDENT = Value("identifier") 199 val ident = (alphanumeric | symbolic) ^^ (x => Token(Kind.IDENT, x))
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_bibtex.scala | 69 case Bibtex.Token.Kind.IDENT =>
|
H A D | jedit_rendering.scala | 50 Token.Kind.IDENT -> NULL, 82 ML_Lex.Kind.IDENT -> NULL,
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_bibtex.scala | 69 case Bibtex.Token.Kind.IDENT =>
|
/seL4-l4v-10.1.1/HOL4/src/IndDef/ |
H A D | IndDefLib.sml | 22 | dest (IDENT (_,s)) = s
|