# HG changeset patch # User wenzelm # Date 1326654239 -3600 # Node ID bed0a3584faf064a1db8813de0179ee7a186a9ac # Parent d0a2c4a80a00f499c5ab4eee921cac7636017423# Parent d8286601e7df9edfe60ad40e1fb23d2533bf6ee4 merged diff -r d8286601e7df -r bed0a3584faf src/HOL/IMP/ACom.thy --- a/src/HOL/IMP/ACom.thy Sun Jan 15 19:55:31 2012 +0100 +++ b/src/HOL/IMP/ACom.thy Sun Jan 15 20:03:59 2012 +0100 @@ -7,7 +7,7 @@ (* is there a better place? *) definition "show_state xs s = [(x,s x). x \ xs]" -section "Annotated Commands" +subsection "Annotated Commands" datatype 'a acom = SKIP 'a ("SKIP {_}" 61) | diff -r d8286601e7df -r bed0a3584faf src/HOL/IMP/Abs_Int0_fun.thy --- a/src/HOL/IMP/Abs_Int0_fun.thy Sun Jan 15 19:55:31 2012 +0100 +++ b/src/HOL/IMP/Abs_Int0_fun.thy Sun Jan 15 20:03:59 2012 +0100 @@ -1,7 +1,5 @@ (* Author: Tobias Nipkow *) -header "Abstract Interpretation" - theory Abs_Int0_fun imports "~~/src/HOL/ex/Interpretation_with_Defs" "~~/src/HOL/Library/While_Combinator" diff -r d8286601e7df -r bed0a3584faf src/HOL/IMP/Complete_Lattice_ix.thy --- a/src/HOL/IMP/Complete_Lattice_ix.thy Sun Jan 15 19:55:31 2012 +0100 +++ b/src/HOL/IMP/Complete_Lattice_ix.thy Sun Jan 15 20:03:59 2012 +0100 @@ -1,7 +1,13 @@ +(* Author: Tobias Nipkow *) + +header "Abstract Interpretation" + theory Complete_Lattice_ix imports Main begin +subsection "Complete Lattice (indexed)" + text{* A complete lattice is an ordered type where every set of elements has a greatest lower (and thus also a leats upper) bound. Sets are the prototypical complete lattice where the greatest lower bound is