# HG changeset patch
# User nipkow
# Date 1367979404 -7200
# Node ID b41268648df2a36fb7783cbf88be992d7e9f6e37
# Parent  a6b963bc46f049a7c11c476864a0cf0fd013b6a6
hide Fin on output

diff -r a6b963bc46f0 -r b41268648df2 src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Tue May 07 21:37:40 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Wed May 08 04:16:44 2013 +0200
@@ -6,6 +6,12 @@
 
 subsection "Interval Analysis"
 
+text{* Drop @{const Fin} around numerals on output: *}
+translations
+"_Numeral i" <= "CONST Fin(_Numeral i)"
+"0" <= "CONST Fin 0"
+"1" <= "CONST Fin 1"
+
 type_synonym eint = "int extended"
 type_synonym eint2 = "eint * eint"
 
@@ -406,11 +412,6 @@
 
 subsubsection "Tests"
 
-(* Hide Fin in numerals on output *)
-declare
-Fin_numeral [code_post] Fin_neg_numeral [code_post]
-zero_extended_def[symmetric, code_post] one_extended_def[symmetric, code_post]
-
 value "show_acom_opt (AI_ivl test1_ivl)"
 
 text{* Better than @{text AI_const}: *}