From 505b93b7cb8783d29883089e84773271f59abf52 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Fri, 22 Aug 2014 18:10:22 -0700
Subject: [PATCH] refactor(lean/examples/constable.lean): move to
 library/standard/logic/examples/nuprl_examples.lean

---
 .../standard/logic/connectives/instances.lean   | 14 --------------
 library/standard/logic/examples/examples.md     |  4 ++++
 .../standard/logic/examples/nuprl_examples.lean |  0
 library/standard/logic/logic.md                 |  3 ++-
 library/standard/tools/helper_tactics.lean      | 17 +++++++++++++++++
 5 files changed, 23 insertions(+), 15 deletions(-)
 create mode 100644 library/standard/logic/examples/examples.md
 rename examples/standard/constable.lean => library/standard/logic/examples/nuprl_examples.lean (100%)
 create mode 100644 library/standard/tools/helper_tactics.lean

diff --git a/library/standard/logic/connectives/instances.lean b/library/standard/logic/connectives/instances.lean
index f25009f36..69fb01a58 100644
--- a/library/standard/logic/connectives/instances.lean
+++ b/library/standard/logic/connectives/instances.lean
@@ -131,18 +131,4 @@ namespace iff_ops
   abbreviation subst := @subst_iff
   abbreviation mp    := @iff_mp
 end iff_ops
-
-
--- Boolean calculations
--- --------------------
-
--- TODO: move these somewhere
-
-theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
-calc
-  (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc _ _ _
-    ... ↔ a ∨ (c ∨ b) : {or_comm b c}
-     ... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
-
--- TODO: add or_left_comm, and_right_comm, and_left_comm
 end relation
diff --git a/library/standard/logic/examples/examples.md b/library/standard/logic/examples/examples.md
new file mode 100644
index 000000000..8cf5cdde4
--- /dev/null
+++ b/library/standard/logic/examples/examples.md
@@ -0,0 +1,4 @@
+logic.examples
+==============
+
+* [nuprl_examples](nuprl_examples.lean) : examples from "Logical investigations with the Nuprl Proof Assistant"
diff --git a/examples/standard/constable.lean b/library/standard/logic/examples/nuprl_examples.lean
similarity index 100%
rename from examples/standard/constable.lean
rename to library/standard/logic/examples/nuprl_examples.lean
diff --git a/library/standard/logic/logic.md b/library/standard/logic/logic.md
index 0d0ea1203..8638073d3 100644
--- a/library/standard/logic/logic.md
+++ b/library/standard/logic/logic.md
@@ -5,4 +5,5 @@ Logical constructions and axioms. By default, `import logic` does not import any
 
 * [connectives](connectives/connectives.md) : logical connectives
 * [axioms](axioms/axioms.md) : additional axioms
-* [classes](classes/classes.md) : classes for inhabited types, decidable types, etc.
\ No newline at end of file
+* [classes](classes/classes.md) : classes for inhabited types, decidable types, etc.
+* [examples](examples/examples.md)
\ No newline at end of file
diff --git a/library/standard/tools/helper_tactics.lean b/library/standard/tools/helper_tactics.lean
new file mode 100644
index 000000000..83178f734
--- /dev/null
+++ b/library/standard/tools/helper_tactics.lean
@@ -0,0 +1,17 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura, Jeremy Avigad
+
+-- tools.helper_tactics
+-- ====================
+
+-- Useful tactics.
+
+import .tactic
+
+using tactic
+
+namespace helper_tactics
+  definition apply_refl := apply @refl
+  tactic_hint apply_refl
+end helper_tactics