src/Pure/ProofGeneral/ROOT.ML
author haftmann
Fri, 24 Apr 2009 17:45:17 +0200
changeset 30973 304ab57afa6e
parent 29929 9e903a645d8f
child 30980 fe0855471964
permissions -rw-r--r--
observe distinction between Pure/Tools and Tools more closely
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21943
b7b66f440d04 added proper header;
wenzelm
parents: 21867
diff changeset
     1
(*  Title:      Pure/ProofGeneral/ROOT.ML
b7b66f440d04 added proper header;
wenzelm
parents: 21867
diff changeset
     2
    Author:     David Aspinall
b7b66f440d04 added proper header;
wenzelm
parents: 21867
diff changeset
     3
24529
afd2be8a9aba use preferences.ML: do setmp *here*, to capture intended default values;
wenzelm
parents: 23793
diff changeset
     4
Proof General interface for Isabelle, both the traditional Emacs version,
afd2be8a9aba use preferences.ML: do setmp *here*, to capture intended default values;
wenzelm
parents: 23793
diff changeset
     5
and PGIP experiments.
21943
b7b66f440d04 added proper header;
wenzelm
parents: 21867
diff changeset
     6
*)
b7b66f440d04 added proper header;
wenzelm
parents: 21867
diff changeset
     7
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     8
use "pgip_types.ML";
23610
5ade06703b07 Produce good PGML 2.0
aspinall
parents: 23570
diff changeset
     9
use "pgml.ML";
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    10
use "pgip_markup.ML";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    11
use "pgip_input.ML";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    12
use "pgip_output.ML";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    13
use "pgip.ML";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    14
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    15
use "pgip_isabelle.ML";
25375
9482ef88e5bc ProofGeneral/preferences: auto_quickcheck=true;
wenzelm
parents: 25275
diff changeset
    16
9482ef88e5bc ProofGeneral/preferences: auto_quickcheck=true;
wenzelm
parents: 25275
diff changeset
    17
(use
9482ef88e5bc ProofGeneral/preferences: auto_quickcheck=true;
wenzelm
parents: 25275
diff changeset
    18
  |> setmp Proofterm.proofs 1
9482ef88e5bc ProofGeneral/preferences: auto_quickcheck=true;
wenzelm
parents: 25275
diff changeset
    19
  |> setmp quick_and_dirty true
30973
304ab57afa6e observe distinction between Pure/Tools and Tools more closely
haftmann
parents: 29929
diff changeset
    20
  |> setmp Quickcheck.auto true
29929
9e903a645d8f enable auto-solve by default
kleing
parents: 29858
diff changeset
    21
  |> setmp auto_solve true) "preferences.ML";
25375
9482ef88e5bc ProofGeneral/preferences: auto_quickcheck=true;
wenzelm
parents: 25275
diff changeset
    22
23793
b04afc51914c added ProofGeneral/pgip_parser.ML;
wenzelm
parents: 23610
diff changeset
    23
use "pgip_parser.ML";
b04afc51914c added ProofGeneral/pgip_parser.ML;
wenzelm
parents: 23610
diff changeset
    24
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21642
diff changeset
    25
use "pgip_tests.ML";
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21642
diff changeset
    26
24529
afd2be8a9aba use preferences.ML: do setmp *here*, to capture intended default values;
wenzelm
parents: 23793
diff changeset
    27
use "proof_general_pgip.ML";
afd2be8a9aba use preferences.ML: do setmp *here*, to capture intended default values;
wenzelm
parents: 23793
diff changeset
    28
use "proof_general_emacs.ML";
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21642
diff changeset
    29