From d59dabaf7c005a3f09cdec80dbd09d913742b19e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Tue, 6 Feb 2024 11:01:16 +0100
Subject: [PATCH] Cleanup

---
 Isabelle_DOF/thys/RegExpInterface.thy | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/Isabelle_DOF/thys/RegExpInterface.thy b/Isabelle_DOF/thys/RegExpInterface.thy
index 6ad24f6..3bb1ed7 100644
--- a/Isabelle_DOF/thys/RegExpInterface.thy
+++ b/Isabelle_DOF/thys/RegExpInterface.thy
@@ -52,12 +52,6 @@ definition rep1 :: "'a rexp \<Rightarrow> 'a rexp" ("\<lbrace>(_)\<rbrace>\<^sup
 definition opt :: "'a rexp \<Rightarrow> 'a rexp" ("\<lbrakk>(_)\<rbrakk>")
    where "\<lbrakk>A\<rbrakk> \<equiv>  A || One"
 
-find_consts name:"RegExpI*"
-
-ML\<open>
-val t = Sign.syn_of \<^theory>
-\<close>
-print_syntax
 value "Star (Conc(Alt (Atom(CHR ''a'')) (Atom(CHR ''b''))) (Atom(CHR ''c'')))"
 text\<open>or better equivalently:\<close>
 value "\<lbrace>(\<lfloor>CHR ''a''\<rfloor> || \<lfloor>CHR ''b''\<rfloor>) ~~ \<lfloor>CHR ''c''\<rfloor>\<rbrace>\<^sup>*"