comment examples

tests/one_shot.v

@@ -6,6 +6,9 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Import par.
 Set Default Proof Using "Type".
 
+(** This is the introductory example from the "Iris from the Ground Up" journal
+paper. *)
+
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
   (* tryset *) (λ: "n",

tests/one_shot_once.v

@@ -6,6 +6,9 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Import par.
 Set Default Proof Using "Type".
 
+(** This is the introductory example from Ralf's PhD thesis.
+The difference to [one_shot] is that [set] asserts to be called only once. *)
+
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
   (* set *) (λ: "n",