Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/main'
Browse files Browse the repository at this point in the history
  • Loading branch information
simondfoster committed Jan 30, 2024
2 parents 2246b24 + 2bdd0f5 commit 1bdaa62
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Expressions.thy
Original file line number Diff line number Diff line change
Expand Up @@ -304,7 +304,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

0 comments on commit 1bdaa62

Please sign in to comment.