Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authornipkow
Tue, 18 Sep 2012 03:33:53 +0200
changeset 49433 1095f240146a
parent 49432 3f4104ccca77
child 49434 433dc7e028c8
tuned
src/HOL/IMP/Abs_Int1_const.thy file | annotate | diff | comparison | revisions
src/HOL/IMP/Abs_Int1_parity.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/IMP/Abs_Int1_const.thy	Tue Sep 18 03:24:51 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Tue Sep 18 03:33:53 2012 +0200
@@ -133,7 +133,7 @@
 
 interpretation Abs_Int_measure
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-and m = m_const and h = "2"
+and m = m_const and h = "1"
 proof
   case goal1 thus ?case by(auto simp: m_const_def split: const.splits)
 next
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Tue Sep 18 03:24:51 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Tue Sep 18 03:33:53 2012 +0200
@@ -155,7 +155,7 @@
 
 interpretation Abs_Int_measure
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-and m = m_parity and h = "2"
+and m = m_parity and h = "1"
 proof
   case goal1 thus ?case by(auto simp add: m_parity_def le_parity_def)
 next
isabelle