git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13760 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Frédéric Tuong 2019-04-03 17:01:17 +00:00
parent 803281d37f
commit 89c191a187
2 changed files with 11 additions and 3 deletions

View File

@ -41,8 +41,9 @@ begin
section \<open>The Construction of an C-Context (analogously to the standard ML context)\<close>
ML\<open>
(* Author: Frédéric Tuong, Université Paris-Saclay *)
(* Title: Pure/Isar/keyword.ML
Author: Frederic Tuong, Makarius
Author: Makarius
Isar keyword classification.
*)
@ -535,8 +536,9 @@ end;
\<close>
ML\<open>
(* Author: Frédéric Tuong, Université Paris-Saclay *)
(* Title: Pure/Thy/thy_header.ML
Author: Frederic Tuong, Makarius
Author: Makarius
Static theory header information.
*)
@ -697,8 +699,9 @@ end
\<close>
ML\<open>
(* Author: Frédéric Tuong, Université Paris-Saclay *)
(* Title: Pure/ML/ml_context.ML
Author: Frederic Tuong, Makarius
Author: Makarius
ML context and antiquotations.
*)

View File

@ -77,6 +77,7 @@ section \<open>Instantiation of the Scanner with C Lexems \<close>
text\<open>Basically copied and modified from files in Pure General of Isabelle.\<close>
ML\<open>
(* Author: Frédéric Tuong, Université Paris-Saclay *)
(* Title: Pure/General/symbol.ML
Author: Makarius
@ -111,6 +112,7 @@ end
\<close>
ML\<open>
(* Author: Frédéric Tuong, Université Paris-Saclay *)
(* Title: Pure/General/symbol_pos.ML
Author: Makarius
@ -215,6 +217,7 @@ end
\<close>
ML\<open>
(* Author: Frédéric Tuong, Université Paris-Saclay *)
(* Title: Pure/General/antiquote.ML
Author: Makarius
@ -338,6 +341,7 @@ end;
\<close>
ML\<open>
(* Author: Frédéric Tuong, Université Paris-Saclay *)
(* Title: Pure/ML/ml_options.ML
Author: Makarius
@ -357,6 +361,7 @@ end
\<close>
ML\<open>
(* Author: Frédéric Tuong, Université Paris-Saclay *)
(* Title: Pure/ML/ml_lex.ML
Author: Makarius