| author | huffman |
| Fri, 13 Sep 2013 14:57:20 -0700 | |
| changeset 53676 | 476ef9b468d2 |
| 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 |