Removed SEXP_sexpr_if from the simplifier

isabelle-utp · Jan 16, 2024 · 2bdd0f5 · 2bdd0f5
1 parent 511ffae
commit 2bdd0f5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Expressions.thy b/Expressions.thy
@@ -297,7 +297,7 @@ lemma expr_if_reach [simp]: "P \<triangleleft> b \<triangleright> (Q \<trianglel
 lemma expr_if_disj [simp]: "P \<triangleleft> b \<triangleright> (P \<triangleleft> c \<triangleright> Q) = P \<triangleleft> b \<or> c \<triangleright> Q"
   by expr_auto
 
-lemma SEXP_expr_if [simp]: "[expr_if P b Q]\<^sub>e = expr_if P b Q"
+lemma SEXP_expr_if: "[expr_if P b Q]\<^sub>e = expr_if P b Q"
   by (simp add: SEXP_def)
 
 end