--- a/src/HOL/Nominal/Examples/Nominal_Examples.thy Fri Sep 12 13:50:55 2014 +0200
+++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy Fri Sep 12 16:42:36 2014 +0200
@@ -3,26 +3,7 @@
header {* Various examples involving nominal datatypes. *}
theory Nominal_Examples
-imports
- CK_Machine
- CR
- CR_Takahashi
- Class3
- Compile
- Contexts
- Crary
- Fsub
- Height
- Lambda_mu
- LocalWeakening
- Pattern
- SN
- SOS
- Standardization
- Support
- Type_Preservation
- W
- Weakening
+imports Nominal_Examples_Base Class3
begin
end