From abd493b93f3da67d034ec3567a84c8f386e55ce9 Mon Sep 17 00:00:00 2001
From: Magdalena Haselsteiner <magdalena.haselsteiner@gmx.at>
Date: Wed, 31 Oct 2018 22:24:55 +0100
Subject: [PATCH] add isabelle program (#778)

---
 LANGUAGES.md            |  1 +
 examples/i/isabelle.thy | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 examples/i/isabelle.thy

diff --git a/LANGUAGES.md b/LANGUAGES.md
index 710b8811..8e23183c 100644
--- a/LANGUAGES.md
+++ b/LANGUAGES.md
@@ -787,6 +787,7 @@ You can also request a new language to be added to the list, just leave a commen
 - [ ] [Iota](http://esolangs.org/wiki/Iota)
 - [ ] [IRC](http://esolangs.org/wiki/IRC)
 - [ ] [Iris](http://esolangs.org/wiki/Iris)
+- [x] [isabelle](https://en.wikipedia.org/wiki/Isabelle_(proof_assistant))
 - [x] [ISCOM](http://esolangs.org/wiki/ISCOM)
 - [ ] [itflabtijtslwi](http://esolangs.org/wiki/Itflabtijtslwi)
 - [x] [IWBASIC](https://rosettacode.org/wiki/Hello_world/Text#IWBASIC)
diff --git a/examples/i/isabelle.thy b/examples/i/isabelle.thy
new file mode 100644
index 00000000..a58a27af
--- /dev/null
+++ b/examples/i/isabelle.thy
@@ -0,0 +1,18 @@
+theory isabelle
+imports Main
+
+begin
+theorem HelloWorld:
+assumes 1: "Meeting \<and> Greeting \<longrightarrow> Hello"
+assumes 2: "Greeting \<longrightarrow> Meeting"
+assumes 3: "Greeting"
+shows "Hello"
+proof - 
+{
+  from 2 3 have 4: "Meeting" by (rule mp)
+  from 4 3 have 5: "Meeting \<and> Greeting" by (rule conjI)
+  from 1 5 have 6: "Hello" by (rule mp)
+}
+thus ?thesis .
+qed
+end
\ No newline at end of file