--- a/src/HOL/IMP/Abs_Int0.thy Mon Aug 20 20:54:40 2018 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Tue Aug 21 17:29:46 2018 +0200
@@ -1,10 +1,12 @@
(* Author: Tobias Nipkow *)
+subsection "Abstract Interpretation"
+
theory Abs_Int0
imports Abs_Int_init
begin
-subsection "Orderings"
+subsubsection "Orderings"
text\<open>The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are
defined in @{theory Main}, more precisely in theories @{theory HOL.Orderings} and @{theory HOL.Lattices}.
@@ -139,7 +141,7 @@
using pfp_inv[OF assms(2), where P = "%x. g x = g x0"] assms(1) by simp
-subsection "Abstract Interpretation"
+subsubsection "Abstract Interpretation"
definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
"\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}"