diff -r ac7dff1194e8 -r 3a5ebb2fcdbf Nominal/Ex/Modules.thy --- a/Nominal/Ex/Modules.thy Mon Sep 20 21:52:45 2010 +0800 +++ b/Nominal/Ex/Modules.thy Wed Sep 22 14:19:48 2010 +0800 @@ -2,14 +2,14 @@ imports "../Nominal2" begin -(* example from Leroy'96 about modules; - see OTT example by Owens *) +(* + example from Leroy'96 about modules + + see OTT example by Owens +*) atom_decl name -declare [[STEPS = 31]] - - nominal_datatype modules: mexp = Acc "path" @@ -72,7 +72,7 @@ thm modules.eq_iff thm modules.fv_bn_eqvt thm modules.size_eqvt - +thm modules.supp end