src/HOL/Import/HOL4Setup.thy
changeset 19064 bf19cc5a7899
parent 17801 30cbd2685e73
child 20326 cbf31171c147
equal deleted inserted replaced
19063:049c010c8fb7 19064:bf19cc5a7899
     1 (*  Title:      HOL/Import/HOL4Setup.thy
     1 (*  Title:      HOL/Import/HOL4Setup.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg (TU Muenchen)
     3     Author:     Sebastian Skalberg (TU Muenchen)
     4 *)
     4 *)
     5 
     5 
     6 theory HOL4Setup imports MakeEqual
     6 theory HOL4Setup imports MakeEqual ImportRecorder
     7   uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML"
     7   uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
     8     ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
       
     9 
     8 
    10 section {* General Setup *}
     9 section {* General Setup *}
    11 
    10 
    12 lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q"
    11 lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q"
    13   by auto
    12   by auto