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

A verified theory for rational numbers representation and simple calculations;
verified with respect to the real numbers;

Fixed bug that caused proof of induction theorem to fail if
introduction rules contained True or False.

minimize imports

clean up polar_Ex proofs; remove unnecessary lemmas

remove simp attribute from various polar_Ex lemmas

tuned proofs

spelling: rename arcos -> arccos

tuned proofs

add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules

generalized sgn function to work on any real normed vector space