# HG changeset patch # User Christian Urban # Date 1259849011 -3600 # Node ID 91c374abde06ff9c9afdef7946a630190fec8172 # Parent 6cdba30c6d66dd3e95655cdfe9c7da8f8374510d removed quot argument...not all examples work anymore diff -r 6cdba30c6d66 -r 91c374abde06 FIXME-TODO --- a/FIXME-TODO Thu Dec 03 14:02:05 2009 +0100 +++ b/FIXME-TODO Thu Dec 03 15:03:31 2009 +0100 @@ -24,7 +24,15 @@ Lower Priority ============== +- allow the user to provide the rsp lemmas in a more + natural form + - find clean ways how to write down the "mathematical" procedure for a possible submission (Peter submitted his work only to TPHOLs 2005...we would have to go - maybe for the Journal of Formalised Mathematics) \ No newline at end of file + maybe for the Journal of Formalised Mathematics) + +- use lower-case letters where appropriate in order + to make Markus happy + +- add tests for adding theorems to the various thm lists \ No newline at end of file diff -r 6cdba30c6d66 -r 91c374abde06 FSet.thy --- a/FSet.thy Thu Dec 03 14:02:05 2009 +0100 +++ b/FSet.thy Thu Dec 03 15:03:31 2009 +0100 @@ -180,7 +180,7 @@ shows "(z memb x) = (z memb y)" using a by induct auto -lemma ho_memb_rsp[quot_rsp]: +lemma ho_memb_rsp[quotient_rsp]: "(op = ===> (op \ ===> op =)) (op memb) (op memb)" by (simp add: memb_rsp) @@ -190,17 +190,17 @@ shows "card1 a = card1 b" using e by induct (simp_all add:memb_rsp) -lemma ho_card1_rsp[quot_rsp]: +lemma ho_card1_rsp[quotient_rsp]: "(op \ ===> op =) card1 card1" by (simp add: card1_rsp) -lemma cons_rsp[quot_rsp]: +lemma cons_rsp[quotient_rsp]: fixes z assumes a: "xs \ ys" shows "(z # xs) \ (z # ys)" using a by (rule list_eq.intros(5)) -lemma ho_cons_rsp[quot_rsp]: +lemma ho_cons_rsp[quotient_rsp]: "(op = ===> op \ ===> op \) op # op #" by (simp add: cons_rsp) @@ -257,7 +257,7 @@ apply (rule append_sym_rsp) done -lemma ho_append_rsp[quot_rsp]: +lemma ho_append_rsp[quotient_rsp]: "(op \ ===> op \ ===> op \) op @ op @" by (simp add: append_rsp) @@ -269,7 +269,7 @@ apply(auto intro: list_eq.intros) done -lemma ho_map_rsp[quot_rsp]: +lemma ho_map_rsp[quotient_rsp]: "(op = ===> op \ ===> op \) map map" by (simp add: map_rsp) @@ -277,7 +277,7 @@ "(map f (a @ b)) \ (map f a) @ (map f b)" by simp (rule list_eq_refl) -lemma ho_fold_rsp[quot_rsp]: +lemma ho_fold_rsp[quotient_rsp]: "(op = ===> op = ===> op = ===> op \ ===> op =) fold1 fold1" apply (auto simp add: FUN_REL_EQ) apply (case_tac "rsp_fold x") @@ -297,13 +297,13 @@ ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] [quot] *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} lemma "IN x EMPTY = False" apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) -apply(tactic {* clean_tac @{context} [quot] 1*}) +apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) +apply(tactic {* clean_tac @{context} 1*}) done lemma "IN x (INSERT y xa) = (x = y \ IN x xa)" @@ -330,7 +330,7 @@ apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) done -ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} +ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) @@ -348,7 +348,7 @@ apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) prefer 2 -apply(tactic {* clean_tac @{context} [quot] 1 *}) +apply(tactic {* clean_tac @{context} 1 *}) apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) @@ -404,6 +404,9 @@ apply (assumption) done +ML {* quot *} +thm quotient_thm + lemma "P (x :: 'a list) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) done @@ -453,14 +456,14 @@ "fset_case \ list_case" (* Probably not true without additional assumptions about the function *) -lemma list_rec_rsp[quot_rsp]: +lemma list_rec_rsp[quotient_rsp]: "(op = ===> (op = ===> op \ ===> op =) ===> op \ ===> op =) list_rec list_rec" apply (auto simp add: FUN_REL_EQ) apply (erule_tac list_eq.induct) apply (simp_all) sorry -lemma list_case_rsp[quot_rsp]: +lemma list_case_rsp[quotient_rsp]: "(op = ===> (op = ===> op \ ===> op =) ===> op \ ===> op =) list_case list_case" apply (auto simp add: FUN_REL_EQ) sorry diff -r 6cdba30c6d66 -r 91c374abde06 IntEx.thy --- a/IntEx.thy Thu Dec 03 14:02:05 2009 +0100 +++ b/IntEx.thy Thu Dec 03 15:03:31 2009 +0100 @@ -13,6 +13,8 @@ apply(auto simp add: mem_def expand_fun_eq) done +thm quotient_thm + thm my_int_equiv print_theorems @@ -129,7 +131,7 @@ apply(auto) done -lemma ho_plus_rsp[quot_rsp]: +lemma ho_plus_rsp[quotient_rsp]: shows "(intrel ===> intrel ===> intrel) my_plus my_plus" by (simp) @@ -139,17 +141,17 @@ ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} -ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] *} +ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *} -ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} -ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *} +ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} +ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *} lemma "PLUS a b = PLUS b a" apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) prefer 2 -apply(tactic {* clean_tac @{context} [quot] 1 *}) +apply(tactic {* clean_tac @{context} 1 *}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) @@ -187,7 +189,7 @@ apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} [quot] 1 *}) +apply(tactic {* clean_tac @{context} 1 *}) done lemma ho_tst: "foldl my_plus x [] = x" @@ -234,12 +236,12 @@ apply (induct t) by (simp_all add: QUOTIENT_ABS_REP[OF a]) -lemma cons_rsp[quot_rsp]: +lemma cons_rsp[quotient_rsp]: "(op \ ===> LIST_REL op \ ===> LIST_REL op \) op # op #" by simp (* I believe it's true. *) -lemma foldl_rsp[quot_rsp]: +lemma foldl_rsp[quotient_rsp]: "((op \ ===> op \ ===> op \) ===> op \ ===> LIST_REL op \ ===> op \) foldl foldl" apply (simp only: FUN_REL.simps) apply (rule allI) @@ -254,37 +256,17 @@ apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *) sorry -lemma nil_listrel_rsp[quot_rsp]: +lemma nil_listrel_rsp[quotient_rsp]: "(LIST_REL R) [] []" by simp -thm LAMBDA_PRS[no_vars] -thm all_prs[no_vars] - -lemma test_all_prs: - "\QUOTIENT R absf repf; f = g\ \ Ball (Respects R) ((absf ---> id) f) = All g" -apply(drule all_prs) -apply(simp) -done - -lemma test: - "\QUOTIENT R1 Abs1 Rep1; QUOTIENT R2 Abs2 Rep2; - (\x. Rep2 (f (Abs1 x))) = lhs \ \ (Rep1 ---> Abs2) lhs = f" -apply - -thm LAMBDA_PRS -apply(drule LAMBDA_PRS) -apply(assumption) -apply(auto) -done - - lemma "foldl PLUS x [] = x" apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) apply(simp only: nil_prs) -apply(tactic {* clean_tac @{context} [quot] 1 *}) +apply(tactic {* clean_tac @{context} 1 *}) done lemma ho_tst2: "foldl my_plus x (h # t) \ my_plus h (foldl my_plus x t)" @@ -296,6 +278,6 @@ apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) apply(simp only: cons_prs[OF QUOTIENT_my_int]) -apply(tactic {* clean_tac @{context} [quot] 1 *}) +apply(tactic {* clean_tac @{context} 1 *}) done diff -r 6cdba30c6d66 -r 91c374abde06 LFex.thy --- a/LFex.thy Thu Dec 03 14:02:05 2009 +0100 +++ b/LFex.thy Thu Dec 03 15:03:31 2009 +0100 @@ -181,35 +181,35 @@ "perm_trm \ (perm::'x prm \ trm \ trm)" (* TODO/FIXME: Think whether these RSP theorems are true. *) -lemma kpi_rsp[quot_rsp]: +lemma kpi_rsp[quotient_rsp]: "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry -lemma tconst_rsp[quot_rsp]: +lemma tconst_rsp[quotient_rsp]: "(op = ===> aty) TConst TConst" sorry -lemma tapp_rsp[quot_rsp]: +lemma tapp_rsp[quotient_rsp]: "(aty ===> atrm ===> aty) TApp TApp" sorry -lemma tpi_rsp[quot_rsp]: +lemma tpi_rsp[quotient_rsp]: "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry -lemma var_rsp[quot_rsp]: +lemma var_rsp[quotient_rsp]: "(op = ===> atrm) Var Var" sorry -lemma app_rsp[quot_rsp]: +lemma app_rsp[quotient_rsp]: "(atrm ===> atrm ===> atrm) App App" sorry -lemma const_rsp[quot_rsp]: +lemma const_rsp[quotient_rsp]: "(op = ===> atrm) Const Const" sorry -lemma lam_rsp[quot_rsp]: +lemma lam_rsp[quotient_rsp]: "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry -lemma perm_kind_rsp[quot_rsp]: +lemma perm_kind_rsp[quotient_rsp]: "(op = ===> akind ===> akind) op \ op \" sorry -lemma perm_ty_rsp[quot_rsp]: +lemma perm_ty_rsp[quotient_rsp]: "(op = ===> aty ===> aty) op \ op \" sorry -lemma perm_trm_rsp[quot_rsp]: +lemma perm_trm_rsp[quotient_rsp]: "(op = ===> atrm ===> atrm) op \ op \" sorry -lemma fv_ty_rsp[quot_rsp]: +lemma fv_ty_rsp[quotient_rsp]: "(aty ===> op =) fv_ty fv_ty" sorry -lemma fv_kind_rsp[quot_rsp]: +lemma fv_kind_rsp[quotient_rsp]: "(akind ===> op =) fv_kind fv_kind" sorry -lemma fv_trm_rsp[quot_rsp]: +lemma fv_trm_rsp[quotient_rsp]: "(atrm ===> op =) fv_trm fv_trm" sorry @@ -261,7 +261,7 @@ apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) prefer 2 -apply(tactic {* clean_tac @{context} quot 1 *}) +apply(tactic {* clean_tac @{context} 1 *}) (* Profiling: ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} @@ -270,7 +270,7 @@ ML_prf {* PolyML.profiling 1 *} ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} *) -apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) +apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) done (* Does not work: @@ -299,8 +299,8 @@ \ P1 mkind \ P2 mty \ P3 mtrm" apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) -apply(tactic {* clean_tac @{context} quot 1 *}) +apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) +apply(tactic {* clean_tac @{context} 1 *}) done print_quotients diff -r 6cdba30c6d66 -r 91c374abde06 QuotMain.thy --- a/QuotMain.thy Thu Dec 03 14:02:05 2009 +0100 +++ b/QuotMain.thy Thu Dec 03 15:03:31 2009 +0100 @@ -155,6 +155,9 @@ declare [[map * = (prod_fun, prod_rel)]] declare [[map "fun" = (fun_map, FUN_REL)]] +lemmas [quotient_thm] = + FUN_QUOTIENT IDENTITY_QUOTIENT LIST_QUOTIENT + ML {* maps_lookup @{theory} "List.list" *} ML {* maps_lookup @{theory} "*" *} ML {* maps_lookup @{theory} "fun" *} @@ -730,12 +733,9 @@ *} ML {* -fun quotient_tac ctxt quot_thms = +fun quotient_tac ctxt = REPEAT_ALL_NEW (FIRST' - [rtac @{thm FUN_QUOTIENT}, - resolve_tac quot_thms, - rtac @{thm IDENTITY_QUOTIENT}, - rtac @{thm LIST_QUOTIENT}, + [resolve_tac (quotient_rules_get ctxt), (* For functional identity quotients, (op = ---> op =) *) (* TODO: think about the other way around, if we need to shorten the relation *) CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))]) @@ -901,7 +901,7 @@ ML {* -fun inj_repabs_tac ctxt quot_thms rel_refl trans2 = +fun inj_repabs_tac ctxt rel_refl trans2 = (FIRST' [ (* "cong" rule of the of the relation / transitivity*) (* (op =) (R a b) (R c d) ----> \R a c; R b d\ *) @@ -933,11 +933,11 @@ (* R (\) (Rep (Abs \)) ----> R (\) (\) *) (* observe ---> *) NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt - THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), + THEN' (RANGE [SOLVES' (quotient_tac ctxt)]))), (* R (t $ \) (t' $ \) ----> APPLY_RSP provided type of t needs lifting *) NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN' - (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), + (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt), quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), (* (op =) (t $ \) (t' $ \) ----> Cong provided type of t does not need lifting *) @@ -961,8 +961,8 @@ *} ML {* -fun all_inj_repabs_tac ctxt quot_thms rel_refl trans2 = - REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2) +fun all_inj_repabs_tac ctxt rel_refl trans2 = + REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) *} section {* Cleaning of the theorem *} @@ -970,8 +970,8 @@ (* TODO: This is slow *) ML {* -fun allex_prs_tac ctxt quot = - (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot) +fun allex_prs_tac ctxt = + (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt) *} ML {* @@ -991,11 +991,11 @@ (* It proves the QUOTIENT assumptions by calling quotient_tac *) ML {* -fun solve_quotient_assum i quot_thms ctxt thm = +fun solve_quotient_assum i ctxt thm = let val tac = (compose_tac (false, thm, i)) THEN_ALL_NEW - (quotient_tac ctxt quot_thms); + (quotient_tac ctxt); val gc = Drule.strip_imp_concl (cprop_of thm); in Goal.prove_internal [] gc (fn _ => tac 1) @@ -1004,7 +1004,7 @@ *} ML {* -fun lambda_allex_prs_simple_conv quot_thms ctxt ctrm = +fun lambda_allex_prs_simple_conv ctxt ctrm = case (term_of ctrm) of ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => let @@ -1015,7 +1015,7 @@ val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; - val te = @{thm eq_reflection} OF [solve_quotient_assum 2 quot_thms ctxt lpi] + val te = @{thm eq_reflection} OF [solve_quotient_assum 2 ctxt lpi] val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te val tl = Thm.lhs_of ts; val (insp, inst) = make_inst (term_of tl) (term_of ctrm); @@ -1032,7 +1032,7 @@ val tyinst = [SOME cty_a, SOME cty_b]; val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; val thm = Drule.instantiate' tyinst tinst @{thm all_prs}; - val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm]; + val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm]; in Conv.rewr_conv ti ctrm end @@ -1045,7 +1045,7 @@ val tyinst = [SOME cty_a, SOME cty_b]; val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; val thm = Drule.instantiate' tyinst tinst @{thm ex_prs}; - val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm]; + val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm]; in Conv.rewr_conv ti ctrm end @@ -1055,12 +1055,12 @@ (* quot stands for the QUOTIENT theorems: *) (* could be potentially all of them *) ML {* -fun lambda_allex_prs_conv quot = - More_Conv.top_conv (lambda_allex_prs_simple_conv quot) +val lambda_allex_prs_conv = + More_Conv.top_conv lambda_allex_prs_simple_conv *} ML {* -fun lambda_allex_prs_tac quot ctxt = CONVERSION (lambda_allex_prs_conv quot ctxt) +fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt) *} (* @@ -1090,13 +1090,14 @@ *) ML {* -fun clean_tac lthy quot = +fun clean_tac lthy = let val thy = ProofContext.theory_of lthy; + val quotients = quotient_rules_get lthy val defs = map (Thm.varifyT o #def) (qconsts_dest thy); - val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot + val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quotients val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; - val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot + val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quotients val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) @@ -1104,7 +1105,7 @@ EVERY' [ (* (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) ----> f *) (* \x\Respects R. (abs ---> id) f ----> \x. f *) - NDT lthy "a" (TRY o lambda_allex_prs_tac quot lthy), + NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), (* NewConst ----> (rep ---> abs) oldConst *) (* Abs (Rep x) ----> x *) @@ -1217,7 +1218,7 @@ ML {* (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) -fun lift_tac lthy rthm rel_eqv quot = +fun lift_tac lthy rthm rel_eqv = ObjectLogic.full_atomize_tac THEN' gen_frees_tac lthy THEN' Subgoal.FOCUS (fn {context, concl, ...} => @@ -1232,8 +1233,8 @@ [rtac rule, RANGE [rtac rthm', regularize_tac lthy rel_eqv, - rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2, - clean_tac lthy quot]] + rtac thm THEN' all_inj_repabs_tac lthy rel_refl trans2, + clean_tac lthy]] end) lthy *} diff -r 6cdba30c6d66 -r 91c374abde06 quotient_info.ML --- a/quotient_info.ML Thu Dec 03 14:02:05 2009 +0100 +++ b/quotient_info.ML Thu Dec 03 15:03:31 2009 +0100 @@ -164,14 +164,14 @@ (* respectfulness lemmas *) structure RspRules = Named_Thms - (val name = "quot_rsp" + (val name = "quotient_rsp" val description = "Respectfulness theorems.") val rsp_rules_get = RspRules.get (* quotient lemmas *) structure QuotientRules = Named_Thms - (val name = "quotient" + (val name = "quotient_thm" val description = "Quotient theorems.") val quotient_rules_get = QuotientRules.get