Rename iris-lecture-notes to lecture_notes, and add it to _CoqProject

README.md

@@ -48,6 +48,8 @@ This repository contains the following case studies:
         stack implementations
 * [spanning-tree](theories/spanning_tree): Proof of a concurrent spanning tree
   algorithm.
+* [lecture-notes](theories/lecture_notes): Coq examples for the
+  [Iris lecture notes](http://iris-project.org/tutorial-material.html).
 
 ## For Developers: How to update the Iris dependency
 

_CoqProject

@@ -7,6 +7,13 @@ theories/barrier/protocol.v
 theories/barrier/example_client.v
 theories/barrier/example_joining_existentials.v
 
+theories/lecture_notes/coq_intro_example_1.v
+
+theories/spanning_tree/graph.v
+theories/spanning_tree/mon.v
+theories/spanning_tree/spanning.v
+theories/spanning_tree/proof.v
+
 theories/logrel/prelude/base.v
 theories/logrel/stlc/lang.v
 theories/logrel/stlc/typing.v
@@ -48,8 +55,3 @@ theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
 theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
 theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
 theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
-
-theories/spanning_tree/graph.v
-theories/spanning_tree/mon.v
-theories/spanning_tree/spanning.v
-theories/spanning_tree/proof.v