Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotMain.thy
changeset 542 fe468f8723fc
parent 541 94deffed619d
child 543 d030c8e19465 
--- a/QuotMain.thy	Fri Dec 04 16:53:11 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 17:15:55 2009 +0100
@@ -460,7 +460,7 @@
 fun equiv_tac rel_eqvs =
   REPEAT_ALL_NEW (FIRST' 
     [resolve_tac rel_eqvs,
-     rtac @{thm IDENTITY_equivp},
+     rtac @{thm identity_equivp},
      rtac @{thm list_equivp}])
 *}
 
@@ -724,7 +724,7 @@
 ML {*
 fun quotient_tac ctxt =
   REPEAT_ALL_NEW (FIRST'
-    [rtac @{thm IDENTITY_Quotient},
+    [rtac @{thm identity_quotient},
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
@@ -895,7 +895,7 @@
       val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
       val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
       val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
-      val thm = Drule.instantiate' ty_inst t_inst @{thm REP_ABS_RSP}
+      val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
       val te = solve_quotient_assums context thm
       val t_inst = map (SOME o (cterm_of thy)) [lhs, rhs];
       val thm = Drule.instantiate' [] t_inst te
nominal2