author | blanchet |
Thu, 11 Sep 2014 19:26:59 +0200 | |
changeset 58309 | a09ec6daaa19 |
parent 52488 | cd65ee49a8ba |
permissions | -rw-r--r-- |
52488
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
diff
changeset
|
1 |
theory Proofs |
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
diff
changeset
|
2 |
imports Pure |
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
diff
changeset
|
3 |
begin |
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
diff
changeset
|
4 |
|
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
diff
changeset
|
5 |
ML "Proofterm.proofs := 2" |
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
diff
changeset
|
6 |
|
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
diff
changeset
|
7 |
end |
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
diff
changeset
|
8 |