doc-src/Tutorial/Datatype/ROOT.ML
author wenzelm
Sat, 01 Jul 2000 19:49:20 +0200
changeset 9226 cbe6144f0f15
parent 5851 15ce4c1c8313
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5851
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     1
use_thy "ABexp";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     2
use"abgoalind.ML";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     3
use"autotac.ML";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     4
result();
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     5
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     6
use_thy "Term";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     7
use"tidproof.ML";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     8
result();
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
     9
use"appmap.ML";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    10
by(induct_tac "ts" 1);
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    11
by(Auto_tac);
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    12
qed"subst_App_map";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    13
Addsimps [subst_App_map];
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    14
result();
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    15
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    16
use_thy"Trie";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    17
use"lookupempty.ML";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    18
qed "lookup_empty";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    19
Addsimps [lookup_empty];
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    20
use"trieAdds.ML";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    21
use"triemain.ML";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    22
use"trieinduct.ML";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    23
use"trieexhaust.ML";
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    24
by(Auto_tac);
15ce4c1c8313 New section on advanced datatypes.
nipkow
parents:
diff changeset
    25
result();