src/HOL/Import/Generate-HOL/GenHOL4Prob.thy
author skalberg
Fri, 02 Apr 2004 17:37:45 +0200
changeset 14516 a183dec876ab
child 14620 1be590fd2422
permissions -rw-r--r--
Added HOL proof importer.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     1
theory GenHOL4Prob = GenHOL4Real:
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     2
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     3
import_segment "hol4";
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     4
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     5
setup_dump "../HOL" "HOL4Prob";
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     6
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
append_dump "theory HOL4Prob = HOL4Real:";
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
import_theory prob_extra;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
const_moves
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    12
  COMPL > GenHOL4Base.pred_set.COMPL;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
import_theory prob_canon;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    18
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    19
import_theory boolean_sequence;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    20
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
import_theory prob_algebra;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
import_theory prob;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    27
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    28
import_theory prob_pseudo;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    29
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    31
import_theory prob_indep;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    32
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    33
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    34
import_theory prob_uniform;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    35
end_import;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    36
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    37
append_dump "end";
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    38
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    39
flush_dump;
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    40
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    41
import_segment "";
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    42
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    43
end