This commit is contained in:
Burkhart Wolff 2019-03-22 12:29:47 +00:00
parent 98e67422b9
commit 04991c5dc1
2 changed files with 5 additions and 4 deletions

View File

@ -188,7 +188,7 @@ val scan_sym_ident_not_stack = Scan.one (fn c => C_Token.is_sym_ident c andalso
not (C_Token.is_exec_shift c))
>> (fn tok => (C_Token.content_of tok, C_Token.pos_of tok))
fun command cmd scan f =
C0_Outer_Syntax.command' cmd "" (K (Scan.option (Scan.one C_Token.is_colon) -- (scan >> f)
C_Annot_Syntax.command' cmd "" (K (Scan.option (Scan.one C_Token.is_colon) -- (scan >> f)
>> K Never))
in
val _ = Theory.setup ( command ("INVARIANT", \<^here>) C_Parse.term Invariant

View File

@ -42,7 +42,7 @@ section \<open>The Construction of an C-Context (analogously to the standard ML
ML\<open>
(* Title: Pure/Isar/keyword.ML
Author: Makarius
Author: Frederic Tuong, Makarius
Isar keyword classification.
*)
@ -536,7 +536,7 @@ end;
ML\<open>
(* Title: Pure/Thy/thy_header.ML
Author: Makarius
Author: Frederic Tuong, Makarius
Static theory header information.
*)
@ -565,6 +565,7 @@ end
ML\<open>
(* Title: Pure/Isar/outer_syntax.ML
Author: Frederic Tuong, Univ. Paris-Saclay
Author: Markus Wenzel, TU Muenchen
Isabelle/Isar outer syntax.
@ -690,7 +691,7 @@ end
ML\<open>
(* Title: Pure/ML/ml_context.ML
Author: Makarius
Author: Frederic Tuong, Makarius
ML context and antiquotations.
*)