1.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Tue Jan 05 17:29:39 2021 +0100
     1.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Wed Jan 06 11:17:28 2021 +0100
     1.3 @@ -161,7 +161,7 @@
     1.4  ## calling Output.report
     1.5  \<close>
     1.6  
     1.7 -subsection \<open>fill gaps in traces \<close>
     1.8 +subsection \<open>fill gaps in traces\<close>
     1.9  subsubsection \<open>at beginning of "have "0 \<le> c mod d""\<close>
    1.10  text \<open>
    1.11    WHAT HAS BEEN OBSERVED / DONE
    1.12 @@ -183,10 +183,10 @@
    1.13      Syntax.read_props callers..
    1.14        in Syntax.:
    1.15          read_prop
    1.16 -          read_prop_global:                     not in trace--//
    1.17 +          read_prop_global:                     not in trace--|
    1.18        in src/Pure (NO "open Syntax")
    1.19 -        Expression.read_full_context_statement  not in trace--//
    1.20 -        Proof_Context.read_propp                not in trace--//
    1.21 +        Expression.read_full_context_statement  not in trace--|
    1.22 +        Proof_Context.read_propp                not in trace--|
    1.23          ML_Thms: val _ = Theory.setup..thm_binding "lemma"..propss:
    1.24                                                  ?in trace ?!?
    1.25            TODO ?!?
    1.26 @@ -197,9 +197,9 @@
    1.27      TODO
    1.28      Proof_Context.prep_statement callers..
    1.29        in Proof_Context.:
    1.30 -          cert_statement                        not in trace--//
    1.31 -          read_statement                        not in trace--//
    1.32 -      in src/Pure (NO "open Proof_Context")     ..\<nexists> ----------//
    1.33 +          cert_statement                        not in trace--|
    1.34 +          read_statement                        not in trace--|
    1.35 +      in src/Pure (NO "open Proof_Context")     ..\<nexists> ----------|
    1.36          TODO ?!?
    1.37          TODO ?!?
    1.38          TODO ?!?