src/HOL/Main.thy
changeset 28091 50f2d6ba024c
parent 27367 a75d71c73362
child 28228 7ebe8dc06cbb
equal deleted inserted replaced
28090:29af3c712d2b 28091:50f2d6ba024c
     3 *)
     3 *)
     4 
     4 
     5 header {* Main HOL *}
     5 header {* Main HOL *}
     6 
     6 
     7 theory Main
     7 theory Main
     8 imports Plain Map Presburger Recdef
     8 imports Plain Map Nat_Int_Bij Recdef
     9 begin
     9 begin
    10 
    10 
    11 ML {* val HOL_proofs = ! Proofterm.proofs *}
    11 ML {* val HOL_proofs = ! Proofterm.proofs *}
    12 
    12 
    13 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    13 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}