Skip to content

Instantly share code, notes, and snippets.

@KevinKu

KevinKu/Logic_Answer

Created November 5, 2017 07:17
Show Gist options
  • Save KevinKu/1d616da32f974a16bce53be8e5653ec1 to your computer and use it in GitHub Desktop.
Save KevinKu/1d616da32f974a16bce53be8e5653ec1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Logic_Answer
theory Example imports Main
begin
lemma "P∧Q⟹Q∧P"
apply (erule conjE)
apply (rule conjI)
apply assumption
apply assumption
done
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment