# HG changeset patch
# User nipkow
# Date 1367457227 -7200
# Node ID 7e9265a0eb0102507a4e895e9318e6cbf51c5538
# Parent  106afdf5806c9e77d72fc5156a702bad1e553842
tuned

diff -r 106afdf5806c -r 7e9265a0eb01 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Wed May 01 19:33:49 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Thu May 02 03:13:47 2013 +0200
@@ -50,11 +50,11 @@
 fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
 and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
 and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
-assumes test_num': "test_num' n a = (n : \<gamma> a)"
-and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \<Longrightarrow>
-  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
-and filter_less': "filter_less' (n1<n2) a1 a2 = (b1,b2) \<Longrightarrow>
-  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
+assumes test_num': "test_num' i a = (i : \<gamma> a)"
+and filter_plus': "filter_plus' a a1 a2 = (a\<^isub>1',a\<^isub>2') \<Longrightarrow>
+  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1+i2 : \<gamma> a \<Longrightarrow> i1 : \<gamma> a\<^isub>1' \<and> i2 : \<gamma> a\<^isub>2'"
+and filter_less': "filter_less' (i1<i2) a1 a2 = (a\<^isub>1',a\<^isub>2') \<Longrightarrow>
+  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1 : \<gamma> a\<^isub>1' \<and> i2 : \<gamma> a\<^isub>2'"
 
 
 locale Abs_Int1 = Val_abs1 where \<gamma> = \<gamma>