src/HOL/Tools/Quotient/quotient_tacs.ML
changeset 47308 9caab698dbe4
parent 46468 4db76d47b51a
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Apr 03 14:09:37 2012 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Apr 03 16:26:48 2012 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  
     1.5  fun quotient_tac ctxt =
     1.6    (REPEAT_ALL_NEW (FIRST'
     1.7 -    [rtac @{thm identity_quotient},
     1.8 +    [rtac @{thm identity_quotient3},
     1.9       resolve_tac (Quotient_Info.quotient_rules ctxt)]))
    1.10  
    1.11  fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
    1.12 @@ -259,7 +259,7 @@
    1.13                val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
    1.14                val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
    1.15                val inst_thm = Drule.instantiate' ty_inst
    1.16 -                ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
    1.17 +                ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
    1.18              in
    1.19                (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
    1.20              end
    1.21 @@ -529,7 +529,7 @@
    1.22      val prs = Quotient_Info.prs_rules lthy
    1.23      val ids = Quotient_Info.id_simps lthy
    1.24      val thms =
    1.25 -      @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
    1.26 +      @{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
    1.27  
    1.28      val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
    1.29    in