Searched refs:IDENT (Results 1 - 25 of 34) sorted by relevance

12

/seL4-l4v-10.1.1/isabelle/Admin/lib/Tools/
H A Dmakedist95 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 Dmakedist95 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 DAbsyn_dtype.sml12 | IDENT of locn.locn * string
H A DAbsyn.sml30 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 DTermParse.sml113 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 Dparmonadsyntax.sml44 | 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 Dmonadsyntax.sml134 | 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 Dboolpp.sml246 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 Dabs_tools.sml14 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 Dparse.scala80 tok.kind == Token.Kind.IDENT ||
H A Dtoken.scala23 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 Dparse.scala80 tok.kind == Token.Kind.IDENT ||
H A Dtoken.scala23 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 Dholindex.lex68 handle Binarymap.NotFound => IDENT (mkTok I text pos line);
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/
H A DparsePMATCH.sml188 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 DholfootParser.sml72 | 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 Dholfoot.lex66 handle Binarymap.NotFound => IDENT (mkTok I text pos line);
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/
H A Dbibtex.scala326 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 Dbibtex.scala326 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 Dml_lex.scala44 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 Dml_lex.scala44 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 Djedit_bibtex.scala69 case Bibtex.Token.Kind.IDENT =>
H A Djedit_rendering.scala50 Token.Kind.IDENT -> NULL,
82 ML_Lex.Kind.IDENT -> NULL,
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Djedit_bibtex.scala69 case Bibtex.Token.Kind.IDENT =>
/seL4-l4v-10.1.1/HOL4/src/IndDef/
H A DIndDefLib.sml22 | dest (IDENT (_,s)) = s

Completed in 94 milliseconds

12