Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
the rule is not needed due to 1726f46d2aa8
authorkuncar
Thu, 20 Feb 2014 16:56:32 +0100
changeset 55608 18da85199367
parent 55607 332641e48ff4
child 55609 69ac773a467f
the rule is not needed due to 1726f46d2aa8
src/HOL/Tools/Lifting/lifting_def.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Feb 20 16:47:22 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Feb 20 16:56:32 2014 +0100
@@ -39,8 +39,7 @@
     end
     handle Pattern.MATCH => no_tac
 
-    val rules = @{thm is_equality_eq} ::
-      ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
+    val rules = ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
   in
     EVERY' [CSUBGOAL intro_reflp_tac, 
             REPEAT_ALL_NEW (resolve_tac rules)]
isabelle