# HG changeset patch
# User nipkow
# Date 1365179495 -7200
# Node ID bd3358aac5d20ad22cfae3cb4d9686e6e0816951
# Parent  c839ccebf2fbf22aedf33b04ae6d3f9bd9cdf000
tuned document

diff -r c839ccebf2fb -r bd3358aac5d2 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Fri Apr 05 15:13:25 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Fri Apr 05 18:31:35 2013 +0200
@@ -6,7 +6,9 @@
 
 subsection "Orderings"
 
-declare order_trans[trans]
+text{* The basic type classes @{class order}, @{class semilattice_sup} and @{class top} are
+defined in @{theory Main}, more precisely in theories @{theory Orderings} and @{theory Lattices}.
+If you view this theory with jedit, just click on the names to get there. *}
 
 class semilattice = semilattice_sup + top
 
diff -r c839ccebf2fb -r bd3358aac5d2 src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Fri Apr 05 15:13:25 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri Apr 05 18:31:35 2013 +0200
@@ -26,7 +26,7 @@
 definition less_parity where
 "x < y = (x \<le> y \<and> \<not> y \<le> (x::parity))"
 
-text{*\noindent (The type annotation is necessary to fix the type of the polymorphic predicates.)
+text{*\noindent(The type annotation is necessary to fix the type of the polymorphic predicates.)
 
 Now the instance proof, i.e.\ the proof that the definition fulfills
 the axioms (assumptions) of the class. The initial proof-step generates the
@@ -62,7 +62,7 @@
 write out the proof obligations but use the @{text goali} primitive to refer
 to the assumptions of subgoal i and @{text "case?"} to refer to the
 conclusion of subgoal i. The class axioms are presented in the same order as
-in the class definition. *}
+in the class definition. Warning: this is brittle! *}
 
 instance
 proof
diff -r c839ccebf2fb -r bd3358aac5d2 src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Fri Apr 05 15:13:25 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Fri Apr 05 18:31:35 2013 +0200
@@ -1,7 +1,5 @@
 (* Author: Tobias Nipkow *)
 
-header "Abstract Interpretation (ITP)"
-
 theory Abs_Int0_ITP
 imports "~~/src/HOL/ex/Interpretation_with_Defs"
         "~~/src/HOL/Library/While_Combinator"
diff -r c839ccebf2fb -r bd3358aac5d2 src/HOL/IMP/Abs_Int_ITP/Complete_Lattice_ix.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Complete_Lattice_ix.thy	Fri Apr 05 15:13:25 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Complete_Lattice_ix.thy	Fri Apr 05 18:31:35 2013 +0200
@@ -1,6 +1,6 @@
 (* Author: Tobias Nipkow *)
 
-header "Abstract Interpretation"
+header "Abstract Interpretation (ITP)"
 
 theory Complete_Lattice_ix
 imports Main
diff -r c839ccebf2fb -r bd3358aac5d2 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Apr 05 15:13:25 2013 +0200
+++ b/src/HOL/ROOT	Fri Apr 05 18:31:35 2013 +0200
@@ -113,6 +113,8 @@
     "~~/src/HOL/Library/While_Combinator"
     "~~/src/HOL/Library/Char_ord"
     "~~/src/HOL/Library/List_lexord"
+    "~~/src/HOL/Library/Quotient_List"
+    "~~/src/HOL/Library/Extended"
   theories
     BExp
     ASM