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

Added solution to exercise.

*** empty log message ***

tweaks concerned with poly bug-fixing

Replaced the_context() by theory "Presburger" in call of invoke_oracle.

Tuned some proofs.

Added entry in Settings menu for Toplevel.skip_proofs flag.

Some changes to allow skipping of proof scripts.

Proofs needed to be updated because induction now preserves name of
induction variable.

Induction now preserves the name of the induction variable.

simplification tweaks for better arithmetic reasoning