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.
Quot/Examples/IntEx2.thy
changeset 790 3a48ffcf0f9a
parent 767 37285ec4387d
child 913 b1f55dd64481 
--- a/Quot/Examples/IntEx2.thy	Fri Dec 25 00:58:06 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Sat Dec 26 07:15:30 2009 +0100
@@ -1,5 +1,5 @@
 theory IntEx2
-imports "../QuotMain" Nat
+imports "../QuotMain" "../QuotProd" Nat
 (*uses
   ("Tools/numeral.ML")
   ("Tools/numeral_syntax.ML")
@@ -196,7 +196,7 @@
 lemma add:
      "(abs_int (x,y)) + (abs_int (u,v)) =
       (abs_int (x + u, y + v))"
-apply(simp add: plus_int_def)
+apply(simp add: plus_int_def id_simps)
 apply(fold plus_raw.simps)
 apply(rule Quotient_rel_abs[OF Quotient_int])
 apply(rule plus_raw_rsp_aux)
nominal2