equal
deleted
inserted
replaced
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 = MakeEqual |
6 theory HOL4Setup imports MakeEqual |
7 files ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML"): |
7 uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin |
8 |
8 |
9 section {* General Setup *} |
9 section {* General Setup *} |
10 |
10 |
11 lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q" |
11 lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q" |
12 by auto |
12 by auto |