--- a/src/HOL/HOL.thy Thu Sep 15 10:33:35 2005 +0200
+++ b/src/HOL/HOL.thy Thu Sep 15 11:15:52 2005 +0200
@@ -1282,6 +1282,28 @@
setup InductMethod.setup
+subsubsection{*Tags, for the ATP Linkup*}
+
+constdefs
+ tag :: "bool => bool"
+ "tag P == P"
+
+text{*These label the distinguished literals of introduction and elimination
+rules.*}
+
+lemma tagI: "P ==> tag P"
+by (simp add: tag_def)
+
+lemma tagD: "tag P ==> P"
+by (simp add: tag_def)
+
+text{*Applications of "tag" to True and False must go!*}
+
+lemma tag_True: "tag True = True"
+by (simp add: tag_def)
+
+lemma tag_False: "tag False = False"
+by (simp add: tag_def)
end