equal
deleted
inserted
replaced
812 fix zero :: \<open>int\<close> |
812 fix zero :: \<open>int\<close> |
813 assume \<open>!!x. zero + x = x\<close> \<open>!!x. (-x) + x = zero\<close> |
813 assume \<open>!!x. zero + x = x\<close> \<open>!!x. (-x) + x = zero\<close> |
814 then interpret local_fixed: lgrp \<open>(+)\<close> \<open>zero\<close> \<open>minus\<close> |
814 then interpret local_fixed: lgrp \<open>(+)\<close> \<open>zero\<close> \<open>minus\<close> |
815 by unfold_locales |
815 by unfold_locales |
816 thm local_fixed.lone |
816 thm local_fixed.lone |
817 print_dependencies! lgrp \<open>(+)\<close> \<open>0\<close> \<open>minus\<close> + lgrp \<open>(+)\<close> \<open>zero\<close> \<open>minus\<close> |
|
818 } |
817 } |
819 assume \<open>!!x zero. zero + x = x\<close> \<open>!!x zero. (-x) + x = zero\<close> |
818 assume \<open>!!x zero. zero + x = x\<close> \<open>!!x zero. (-x) + x = zero\<close> |
820 then interpret local_free: lgrp \<open>(+)\<close> \<open>zero\<close> \<open>minus\<close> for zero |
819 then interpret local_free: lgrp \<open>(+)\<close> \<open>zero\<close> \<open>minus\<close> for zero |
821 by unfold_locales |
820 by unfold_locales |
822 thm local_free.lone [where ?zero = \<open>0\<close>] |
821 thm local_free.lone [where ?zero = \<open>0\<close>] |