/seL4-l4v-master/HOL4/tools/Holmake/tests/holdep/errors/ |
H A D | comment_unterm.sml | 1 val foo = 3 (* comment here
|
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | holindexData.sml | 14 comment : string option, 30 comment = NONE, 41 comment = comment, 51 comment = comment, 63 comment = comment, 73 comment = comment, [all...] |
H A D | holindexData.sig | 9 comment : string option, 49 comment : string option,
|
H A D | holindex-demo.tex | 86 \commentHOLtm{unique_id}{comment} 87 \commentHOLty{unique_id}{comment} 88 \commentHOLthm{unique_id}{comment} 131 comment = "some lengthy\\comment 295 % Arg 7 : comment 316 % Arg 6 : comment 361 \commentHOLty{type_id_4}{Some short comment}
|
/seL4-l4v-master/isabelle/Admin/ |
H A D | rsyncd.conf | 11 comment = Isabelle website 15 comment = Isabelle distribution 20 comment = Isabelle website
|
/seL4-l4v-master/l4v/isabelle/Admin/ |
H A D | rsyncd.conf | 11 comment = Isabelle website 15 comment = Isabelle distribution 20 comment = Isabelle website
|
/seL4-l4v-master/HOL4/src/1/theory_tests/ |
H A D | mergeGrammarsA2Script.sml | 5 (* see comment at head of mergeGrammarsA1Script for description of what is
|
H A D | mergeGrammarsBScript.sml | 3 (* see comment at head of mergeGrammarsA1Script.sml for explanation of
|
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | update_comments.scala | 4 Update formal comments in outer syntax: \<comment> \<open>...\<close> 18 Symbol.comment + Symbol.space + Symbol.cartouche(Symbol.trim_blanks(tok.content)) 24 if tok.source == "--" || tok.source == Symbol.comment => 30 case tok :: rest if tok.is_formal_comment && tok.source.startsWith(Symbol.comment) =>
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | update_comments.scala | 4 Update formal comments in outer syntax: \<comment> \<open>...\<close> 18 Symbol.comment + Symbol.space + Symbol.cartouche(Symbol.trim_blanks(tok.content)) 24 if tok.source == "--" || tok.source == Symbol.comment => 30 case tok :: rest if tok.is_formal_comment && tok.source.startsWith(Symbol.comment) =>
|
/seL4-l4v-master/isabelle/src/Tools/VSCode/src/ |
H A D | grammar.scala | 50 "comment": { 53 "name": "comment.block.isabelle", 55 "patterns": [{ "include": "#comment" }], 73 "include": "#comment"
|
/seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | grammar.scala | 50 "comment": { 53 "name": "comment.block.isabelle", 55 "patterns": [{ "include": "#comment" }], 73 "include": "#comment"
|
/seL4-l4v-master/isabelle/src/Tools/Metis/scripts/ |
H A D | mlpp | 106 my $comment = 0; 128 elsif ($state eq "comment") { 137 ++$comment; 141 --$comment; 142 if ($comment == 0) { $state = "normal"; } 206 $state = "comment"; 207 ++$comment; 212 die "mlpp: too many comment closers.\n" 243 elsif ($state eq "comment") { 244 die "mlpp: EOF inside comment\ [all...] |
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/scripts/ |
H A D | mlpp | 106 my $comment = 0; 128 elsif ($state eq "comment") { 137 ++$comment; 141 --$comment; 142 if ($comment == 0) { $state = "normal"; } 206 $state = "comment"; 207 ++$comment; 212 die "mlpp: too many comment closers.\n" 243 elsif ($state eq "comment") { 244 die "mlpp: EOF inside comment\ [all...] |
/seL4-l4v-master/seL4/manual/tools/ |
H A D | gen_invocations.py | 39 def generate_prototype(interface_name, method_name, method_id, inputs, outputs, comment): 53 return "%s\n%s %s %s(%s);" % (comment, prefix, return_type, name, param_list) 84 for (interface_name, method_name, method_id, inputs, outputs, _, comment) in methods: 87 method_name, method_id, inputs, outputs, comment)
|
/seL4-l4v-master/graph-refine/graph-to-graph/ |
H A D | convert_loop_bounds.py | 75 comment = 'did not find cached result' 77 comment = 'ignore: failed' 78 lbfs[f][head] = (2**30, comment, old_worker)
|
/seL4-l4v-master/HOL4/src/ring/src/ |
H A D | numRingScript.sml | 34 * of comment. ^^^
|
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | comment.scala | 1 /* Title: Pure/General/comment.scala 14 val COMMENT = Value("formal comment") 21 Set(Symbol.comment, Symbol.comment_decoded, 27 Set(Symbol.comment, Symbol.comment_decoded) 31 def err(): Nothing = error("Malformed formal comment: " + quote(source))
|
H A D | symbol.scala | 495 val comment_decoded = decode(comment) 583 val comment: Symbol = "\\<comment>"
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | comment.scala | 1 /* Title: Pure/General/comment.scala 14 val COMMENT = Value("formal comment") 21 Set(Symbol.comment, Symbol.comment_decoded, 27 Set(Symbol.comment, Symbol.comment_decoded) 31 def err(): Nothing = error("Malformed formal comment: " + quote(source))
|
/seL4-l4v-master/HOL4/examples/PSL/1.01/parser.mosmlyacc/ |
H A D | Lexer.lex | 17 val commentStart = ref 0; (* Start of outermost comment being scanned *) 23 val commentDepth = ref 0; (* Current comment nesting *)
|
/seL4-l4v-master/isabelle/src/Doc/Eisbach/document/ |
H A D | root.tex | 37 \newenvironment{LongComment}[1] % multi-paragraph comment, argument is owner 44 \newenvironment{LongComment}[1]{\expandafter\comment}{\expandafter\endcomment}
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Eisbach/document/ |
H A D | root.tex | 37 \newenvironment{LongComment}[1] % multi-paragraph comment, argument is owner 44 \newenvironment{LongComment}[1]{\expandafter\comment}{\expandafter\endcomment}
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | HOLsexp.lex | 16 %s string comment quotedsymbol; 22 <INITIAL>";" => (YYBEGIN comment; continue()); 76 <comment>\n => (YYBEGIN INITIAL; continue()); 77 <comment>. => (continue());
|
/seL4-l4v-master/HOL4/src/boss/theory_tests/ |
H A D | theory3Script.sml | 48 (* comment out line above, and it works OK *)
|