src/HOL/Tools/Lifting/lifting_info.ML

--- a/src/HOL/Tools/Lifting/lifting_info.ML	Mon Feb 24 23:17:55 2014 +0000
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Tue Feb 25 15:02:19 2014 +0100
@@ -516,6 +516,11 @@
   #> relfexivity_rule_setup
   #> relator_distr_attribute_setup
 
+(* setup fixed invariant rules *)
+
+val _ = Context.>> (fold (Invariant_Commute.add_thm o Transfer.prep_transfer_domain_thm @{context}) 
+  [@{thm composed_equiv_rel_invariant}, @{thm composed_equiv_rel_eq_invariant}])
+
 (* outer syntax commands *)
 
 val _ =