From 80edbd08e13200d2c080ac281d19948bbbcd92e0 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 25 May 2020 17:09:54 +0200
Subject: Reorganize theory structure. In particular, the identity type moves
 out from under Spartan to HoTT. Spartan now only has Pi and Sigma.

---
 spartan/lib/congruence.ML | 16 ----------------
 1 file changed, 16 deletions(-)
 delete mode 100644 spartan/lib/congruence.ML

(limited to 'spartan/lib/congruence.ML')

diff --git a/spartan/lib/congruence.ML b/spartan/lib/congruence.ML
deleted file mode 100644
index bb7348c..0000000
--- a/spartan/lib/congruence.ML
+++ /dev/null
@@ -1,16 +0,0 @@
-signature Sym_Attr_Data =
-sig
-  val name: string
-  val symmetry_rule: thm
-end
-
-functor Sym_Attr (D: Sym_Attr_Data) =
-struct
-  local
-    val distinct_prems = the_single o Seq.list_of o Tactic.distinct_subgoals_tac
-  in
-    val attr = Thm.rule_attribute []
-      (K (fn th => distinct_prems (th RS D.symmetry_rule) handle THM _ => th))
-    val setup = Attrib.setup (Binding.name D.name) (Scan.succeed attr) ""
-  end
-end
-- 
cgit v1.2.3