src/HOL/Main.thy
changeset 28263 69eaa97e7e96
parent 28228 7ebe8dc06cbb
child 29304 5c71a6da989d
equal deleted inserted replaced
28262:aa7ca36d67fd 28263:69eaa97e7e96
     6 
     6 
     7 theory Main
     7 theory Main
     8 imports Plain Code_Eval Map Nat_Int_Bij Recdef
     8 imports Plain Code_Eval Map Nat_Int_Bij Recdef
     9 begin
     9 begin
    10 
    10 
    11 ML {* val HOL_proofs = ! Proofterm.proofs *}
       
    12 
       
    13 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    11 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    14 
    12 
    15 end
    13 end