Changes

Summary

merged
avoid session qualification because no tex is generated when used; tuned sectioning
removed ineffective code declarations

Changeset 68777:d505274da801 by nipkow: merged
Changeset 68776:403dd13cf6e9 by nipkow: avoid session qualification because no tex is generated when used;<br>tuned sectioning
The file was modified	`src/HOL/IMP/AExp.thy` (diff)
The file was modified	`src/HOL/IMP/BExp.thy` (diff)
The file was modified	`src/HOL/IMP/Big_Step.thy` (diff)
The file was modified	`src/HOL/IMP/Compiler2.thy` (diff)
The file was modified	`src/HOL/IMP/Hoare.thy` (diff)
The file was modified	`src/HOL/IMP/Hoare_Examples.thy` (diff)
The file was modified	`src/HOL/IMP/Hoare_Total.thy` (diff)
The file was modified	`src/HOL/IMP/Hoare_Total_EX.thy` (diff)
The file was modified	`src/HOL/IMP/Hoare_Total_EX2.thy` (diff)
The file was modified	`src/HOL/IMP/Live_True.thy` (diff)
The file was modified	`src/HOL/IMP/Poly_Types.thy` (diff)
The file was modified	`src/HOL/IMP/Sec_Type_Expr.thy` (diff)
The file was modified	`src/HOL/IMP/Sec_Typing.thy` (diff)
The file was modified	`src/HOL/IMP/Sec_TypingT.thy` (diff)
The file was modified	`src/HOL/IMP/VCG.thy` (diff)
The file was modified	`src/HOL/IMP/VCG_Total_EX.thy` (diff)
The file was modified	`src/HOL/IMP/VCG_Total_EX2.thy` (diff)
Changeset 68775:8fbfb67f6824 by haftmann: removed ineffective code declarations
The file was modified	`src/HOL/List.thy` (diff)