| author | blanchet |
| Fri, 20 Sep 2013 22:39:30 +0200 | |
| changeset 53766 | b260a0ce7482 |
| 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 |