| author | paulson <lp15@cam.ac.uk> |
| Thu, 27 Feb 2014 16:07:21 +0000 | |
| changeset 55775 | 1557a391a858 |
| 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 |