--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Oct 14 15:01:37 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Oct 14 15:01:41 2013 +0200
@@ -477,6 +477,7 @@
quot_thm - a quotient theorem (Quotient R Abs Rep T)
opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
(in the form "reflp R")
+ opt_par_thm - a parametricity theorem for R
*)
fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy =
@@ -852,6 +853,10 @@
@ (map (Pretty.string_of o Pretty.item o single) errs)))
end
+(*
+ Registers the data in qinfo in the Lifting infrastructure.
+*)
+
fun lifting_restore qinfo ctxt =
let
val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo