summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

Removed legacy ML files in Protocol case study.

LaTeX code is now generated directly from theory files.

Ported ML proof scripts to Isar.

hide internal structures (again);

marked some CRITICAL sections (for multithreading);

added compatibility file for ML systems without multithreading;

interpretation: unfolding of equations;

interpretation: equations are propositions not pairs of terms;

interpretation: unfolding of equations;
interpretation: equations are propositions not pairs of terms;

increase default max heap size for poly to -H 500 (this is what isatest uses,
-H 80 is not enough for HOL on at-mac-poly).