src/HOL/Main.thy
changeset 66817 0b12755ccbb2
parent 66614 1f1c5d85d232
child 66954 0230af0f3c59
     1.1 --- a/src/HOL/Main.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Main.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -6,7 +6,16 @@
     1.4  \<close>
     1.5  
     1.6  theory Main
     1.7 -imports Predicate_Compile Quickcheck_Narrowing Extraction Nunchaku BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD
     1.8 +  imports
     1.9 +    Predicate_Compile
    1.10 +    Quickcheck_Narrowing 
    1.11 +    Extraction
    1.12 +    Nunchaku
    1.13 +    BNF_Greatest_Fixpoint Filter
    1.14 +    Conditionally_Complete_Lattices
    1.15 +    Binomial
    1.16 +    GCD
    1.17 +    Nat_Transfer
    1.18  begin
    1.19  
    1.20  text \<open>