From 5059fe90b04799e50765b1f71f590e6783a03ed0 Mon Sep 17 00:00:00 2001
From: diekmann <c.diekmann@googlemail.com>
Date: Tue, 17 Jun 2014 21:27:03 +0200
Subject: [PATCH 1/3] Added language Isabelle

Isabelle is a generic proof assistant. It is comparables (to some degree) to Coq.

Used in
* diekmann/topoS
* 3of8/sturm
* formare/auctions
* larsrh/hol-falso
* dpthayer/MetaProof

Hello Wolrd example (file must be named HelloWorld.thy):
  theory HelloWorld
  imports Main
  begin
  (*put content here*)
  end
---
 lib/linguist/languages.yml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml
index 42ce978d..aff5e8b0 100644
--- a/lib/linguist/languages.yml
+++ b/lib/linguist/languages.yml
@@ -987,6 +987,12 @@ IRC log:
   - .irclog
   - .weechatlog
 
+Isabelle:
+  type: programming
+  color: "#fdcd00"
+  extensions:
+  - .thy
+
 Io:
   type: programming
   color: "#a9188d"

From d9f17a65ddf895997056642a104e92121e3ff7d7 Mon Sep 17 00:00:00 2001
From: diekmann <diekmann@minicon.net.in.tum.de>
Date: Wed, 18 Jun 2014 09:16:31 +0200
Subject: [PATCH 2/3] Isabelle language - fixed lexer and added sample

Also, Isabelle is very polular in academia.
See for example http://scholar.google.de/scholar?q=isabelle%2FHOL

In around 40 days, the seL4 microkernel [1] with its
Isabelle proofs is (probably) released on github [2].
[1] http://sel4.systems/
[2] https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-June/msg00011.html
---
 lib/linguist/languages.yml      |  1 +
 samples/Isabelle/HelloWorld.thy | 46 +++++++++++++++++++++++++++++++++
 2 files changed, 47 insertions(+)
 create mode 100644 samples/Isabelle/HelloWorld.thy

diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml
index aff5e8b0..8bcffbcc 100644
--- a/lib/linguist/languages.yml
+++ b/lib/linguist/languages.yml
@@ -989,6 +989,7 @@ IRC log:
 
 Isabelle:
   type: programming
+  lexer: Text only
   color: "#fdcd00"
   extensions:
   - .thy
diff --git a/samples/Isabelle/HelloWorld.thy b/samples/Isabelle/HelloWorld.thy
new file mode 100644
index 00000000..7c814dae
--- /dev/null
+++ b/samples/Isabelle/HelloWorld.thy
@@ -0,0 +1,46 @@
+theory HelloWorld
+imports Main
+begin
+
+section{*Playing around with Isabelle*}
+
+text{* creating a lemma with the name hello_world*}
+lemma hello_world: "True" by simp
+
+(*inspecting it*)
+thm hello_world
+
+text{* defining a string constant HelloWorld *}
+
+definition HelloWorld :: "string" where
+  "HelloWorld \<equiv> ''Hello World!''"
+
+(*reversing HelloWorld twice yilds HelloWorld again*)
+theorem "rev (rev HelloWorld) = HelloWorld"
+  by (fact List.rev_rev_ident)
+
+text{*now we delete the already proven List.rev_rev_ident lema and show it by hand*}
+declare List.rev_rev_ident[simp del]
+hide_fact List.rev_rev_ident
+
+(*It's trivial since we can just 'execute' it*)
+corollary "rev (rev HelloWorld) = HelloWorld"
+  apply(simp add: HelloWorld_def)
+  done
+
+text{*does it hold in general?*}
+theorem rev_rev_ident:"rev (rev l) = l"
+  proof(induction l)
+  case Nil thus ?case by simp
+  next
+  case (Cons l ls)
+    assume IH: "rev (rev ls) = ls"
+    have "rev (l#ls) = (rev ls) @ [l]" by simp
+    hence "rev (rev (l#ls)) = rev ((rev ls) @ [l])" by simp
+    also have "\<dots> = [l] @ rev (rev ls)" by simp
+    finally show "rev (rev (l#ls)) = l#ls" using IH by simp
+  qed
+
+corollary "\<forall>(l::string). rev (rev l) = l" by(fastforce intro: rev_rev_ident)
+
+end

From 947f4e1c57332133d2b2904653973f23eca4f97f Mon Sep 17 00:00:00 2001
From: diekmann <diekmann@minicon.net.in.tum.de>
Date: Wed, 18 Jun 2014 09:34:26 +0200
Subject: [PATCH 3/3] alphabetic sorting

---
 lib/linguist/languages.yml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml
index 8bcffbcc..f24b9b79 100644
--- a/lib/linguist/languages.yml
+++ b/lib/linguist/languages.yml
@@ -987,13 +987,6 @@ IRC log:
   - .irclog
   - .weechatlog
 
-Isabelle:
-  type: programming
-  lexer: Text only
-  color: "#fdcd00"
-  extensions:
-  - .thy
-
 Io:
   type: programming
   color: "#a9188d"
@@ -1006,6 +999,13 @@ Ioke:
   extensions:
   - .ik
 
+Isabelle:
+  type: programming
+  lexer: Text only
+  color: "#fdcd00"
+  extensions:
+  - .thy
+
 J:
   type: programming
   lexer: Text only