diff --git a/MyCommentedIsabelle.thy b/MyCommentedIsabelle.thy index a4411ba7..b01d22f9 100644 --- a/MyCommentedIsabelle.thy +++ b/MyCommentedIsabelle.thy @@ -406,6 +406,8 @@ As one can see, check-routines internally generate the markup. section\Front End \ +ML\Sign.add_trrules\ + subsection\string, bstring and xstring\ text\@{ML_type "string"} is the basic library type from the SML library in structure @{ML_structure "String"}. Many Isabelle operations produce