isabelle: Changelog

traytel [Thu, 30 Jan 2014 12:27:42 +0100] rev 55173

define ofilter outside of wo_rel

haftmann [Thu, 30 Jan 2014 10:00:53 +0100] rev 55172

more direct simplification rules for 1 div/mod numeral; added simplification rules for (- 1) div/mod numeral

blanchet [Thu, 30 Jan 2014 01:03:55 +0100] rev 55171

systematically suppress tracing if asked for (affects 'meson' proof method)

blanchet [Thu, 30 Jan 2014 00:59:12 +0100] rev 55170

silenced reconstructors in Sledgehammer

blanchet [Wed, 29 Jan 2014 23:24:34 +0100] rev 55169

proper 'show' detection

blanchet [Wed, 29 Jan 2014 22:34:34 +0100] rev 55168

correctly handle exceptions arising from (experimental) Isar proof code

haftmann [Wed, 29 Jan 2014 20:11:38 +0100] rev 55167

made smlnj happy

paulson <lp15@cam.ac.uk> [Wed, 29 Jan 2014 17:09:46 +0000] rev 55166

Merge

paulson <lp15@cam.ac.uk> [Wed, 29 Jan 2014 17:09:01 +0000] rev 55165

Removed a dependence upon Old_Number_Theory. Simplified a few proofs.

traytel [Wed, 29 Jan 2014 16:47:06 +0100] rev 55164

merged

isabelle