# HG changeset patch
# User nipkow
# Date 1366479004 -7200
# Node ID 8417feab782efaa8412ec888b415797aeaa92b85
# Parent  cdc05fc4cd0decaab7b6a79b2d46c508ba77b06e
tuned

diff -r cdc05fc4cd0d -r 8417feab782e src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Fri Apr 19 12:04:57 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Sat Apr 20 19:30:04 2013 +0200
@@ -159,7 +159,7 @@
 
 type_synonym 'av st = "(vname \<Rightarrow> 'av)"
 
-locale Abs_Int_Fun = Val_abs \<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
+locale Abs_Int_fun = Val_abs \<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
 begin
 
 fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
@@ -242,7 +242,7 @@
 lemma mono_post: "C1 \<le> C2 \<Longrightarrow> post C1 \<le> post C2"
 by(induction C1 C2 rule: less_eq_acom.induct) (auto)
 
-locale Abs_Int_Fun_mono = Abs_Int_Fun +
+locale Abs_Int_fun_mono = Abs_Int_fun +
 assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
 begin