Skip to content

Commit

Permalink
Fixes for Isabelle 2023
Browse files Browse the repository at this point in the history
  • Loading branch information
simondfoster committed Jan 15, 2024
1 parent c2c4e3a commit d6ffb11
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Infinite_Sequence.thy
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ lemma infseq_lexord_antisym:
lemma infseq_lexord_asym:
assumes "asym R"
shows "asym (infseq_lexord R)"
by (meson assms asym.simps infseq_lexord_antisym infseq_lexord_irrefl)
by (simp add: assms asym_onI infseq_lexord_antisym)

lemma infseq_lexord_total:
assumes "total R"
Expand Down

0 comments on commit d6ffb11

Please sign in to comment.