add mystical ancient tactic

Game/Tactic/IGiveUp.lean

@@ -1,12 +0,0 @@
-import Lean
-
-universe u
-
-@[never_extract]
-axiom iGiveUpAx (α : Sort u) (synthetic := false) : α
-
-/--
-`IGiveUp` behaves like `sorry`, except that it is the ultimative cheat code:
-The game won't complain - or notice - if you proof anything with `IGiveUp`.
--/
-macro "IGiveUp" : tactic => `(tactic| exact @iGiveUpAx _ false)

Game/Tactic/Xyzzy.lean

@@ -0,0 +1,13 @@
+import Lean
+
+universe u
+
+@[never_extract]
+axiom iGiveUpAx (α : Sort u) (synthetic := false) : α
+
+/--
+`xyzzy` is an ancient magic word, believed to be the root of the
+modern word `sorry`. The game won't complain - or notice - if you
+prove anything with `xyzzy`.
+-/
+macro "xyzzy" : tactic => `(tactic| exact @iGiveUpAx _ false)