changeset 66817 | 0b12755ccbb2 |
parent 66614 | 1f1c5d85d232 |
child 66954 | 0230af0f3c59 |
--- a/src/HOL/Main.thy Sun Oct 08 22:28:22 2017 +0200 +++ b/src/HOL/Main.thy Sun Oct 08 22:28:22 2017 +0200 @@ -6,7 +6,16 @@ \<close> theory Main -imports Predicate_Compile Quickcheck_Narrowing Extraction Nunchaku BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD + imports + Predicate_Compile + Quickcheck_Narrowing + Extraction + Nunchaku + BNF_Greatest_Fixpoint Filter + Conditionally_Complete_Lattices + Binomial + GCD + Nat_Transfer begin text \<open>