--- 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
--- 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
--- 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"
--- 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
--- 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