| author | haftmann |
| Sat, 25 Oct 2014 19:20:28 +0200 | |
| changeset 58786 | fa5b67fb70ad |
| 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 |