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 rules are not needed due to 1726f46d2aa8
authorkuncar
Tue, 25 Feb 2014 15:02:54 +0100
changeset 55733 e6edd47f1483
parent 55732 07906fc6af7a
child 55734 3f5b2745d659
the rules are 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	Tue Feb 25 15:02:20 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Feb 25 15:02:54 2014 +0100
@@ -29,7 +29,7 @@
 
 fun mono_eq_prover ctxt prop =
   let
-    val rules = ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
+    val rules = Lifting_Info.get_reflexivity_rules ctxt
   in
     SOME (Goal.prove ctxt [] [] prop (K (REPEAT_ALL_NEW (resolve_tac rules) 1)))
       handle ERROR _ => NONE
isabelle