From 4e601acd45df59b56ea52145f7f87f098554b3c9 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Fri, 24 Aug 2018 21:58:32 +0200
Subject: [PATCH] comments

---
 MyCommentedIsabelle.thy | 2 ++
 1 file changed, 2 insertions(+)

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\<open>Front End \<close>  
 
+ML\<open>Sign.add_trrules\<close>
+
 subsection\<open>string, bstring and xstring\<close>
 text\<open>@{ML_type "string"} is the basic library type from the SML library
 in structure @{ML_structure "String"}. Many Isabelle operations produce