changeset 52733 | 98f94010d78d |
parent 52421 | 6d93140a206c |
child 53071 | 1958a5e65ea5 |
--- a/src/Doc/IsarImplementation/ML.thy Sat Jul 27 16:35:51 2013 +0200 +++ b/src/Doc/IsarImplementation/ML.thy Sat Jul 27 16:44:40 2013 +0200 @@ -251,7 +251,7 @@ T}, with variants as for types \item certified terms are called @{ML_text ct}, rarely @{ML_text - t}, with variants as for terms + t}, with variants as for terms (never @{ML_text ctrm}) \item theorems are called @{ML_text th}, or @{ML_text thm}