From b243f302526a22e8b4b8f2c497e7ffa9f3912e1b Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Sun, 30 Jan 2022 20:57:59 +0100
Subject: [PATCH] changed 'L' - operator to 'Lang' in order to avoid name
 conflicts in papers.

---
 src/DOF/RegExpInterface.thy | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/DOF/RegExpInterface.thy b/src/DOF/RegExpInterface.thy
index 1bbdfe71..81c81f74 100755
--- a/src/DOF/RegExpInterface.thy
+++ b/src/DOF/RegExpInterface.thy
@@ -68,13 +68,13 @@ This universe of denotations is in our concrete case:\<close>
 
 text\<open>Now the denotational semantics for regular expression can be defined on a post-card:\<close>
 
-fun       L :: "'a rexp => 'a lang"
-  where   L_Emp :   "L Zero        = {}"
-         |L_One:    "L One         = {[]}"
-         |L_Atom:   "L (\<lfloor>a\<rfloor>)       = {[a]}"
-         |L_Un:     "L (el || er)  = (L el) \<union> (L er)"
-         |L_Conc:   "L (el ~~ er)  = {xs@ys | xs ys. xs \<in> L el \<and> ys \<in> L er}"
-         |L_Star:   "L (Star e)    = Regular_Set.star(L e)"
+fun       Lang :: "'a rexp => 'a lang"
+  where   L_Emp :   "Lang Zero        = {}"
+         |L_One:    "Lang One         = {[]}"
+         |L_Atom:   "Lang (\<lfloor>a\<rfloor>)       = {[a]}"
+         |L_Un:     "Lang (el || er)  = (Lang el) \<union> (Lang er)"
+         |L_Conc:   "Lang (el ~~ er)  = {xs@ys | xs ys. xs \<in> Lang el \<and> ys \<in> Lang er}"
+         |L_Star:   "Lang (Star e)    = Regular_Set.star(Lang e)"
 
 
 text\<open>A more useful definition is the sub-language - definition\<close>