src/HOL/Import/Generate-HOL/GenHOL4Vec.thy
author wenzelm
Wed, 21 Sep 2005 18:04:49 +0200
changeset 17566 484ff733f29c
parent 16417 9bc16273c2d4
child 41589 bbd861837ebc
permissions -rw-r--r--
new header syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14620
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14516
diff changeset
     1
(*  Title:      HOL/Import/Generate-HOL/GenHOL4Vec.thy
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14516
diff changeset
     2
    ID:         $Id$
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14516
diff changeset
     3
    Author:     Sebastian Skalberg (TU Muenchen)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14516
diff changeset
     4
*)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents: 14516
diff changeset
     5
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14620
diff changeset
     6
theory GenHOL4Vec imports GenHOL4Base begin
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
import_segment "hol4";
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
setup_dump "../HOL" "HOL4Vec";
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
17566
484ff733f29c new header syntax;
wenzelm
parents: 16417
diff changeset
    12
append_dump "theory HOL4Vec imports HOL4Base begin";
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
import_theory res_quan;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
import_theory word_base;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    18
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    19
const_renames
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    20
  BIT > bit;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
import_theory word_num;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    27
import_theory word_bitop;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    28
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    29
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
import_theory bword_num;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    31
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    32
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    33
import_theory bword_arith;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    34
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    35
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    36
import_theory bword_bitop;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    37
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    38
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    39
append_dump "end";
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    40
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    41
flush_dump;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    42
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    43
import_segment "";
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    44
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    45
end