blanchet [Thu, 13 Mar 2014 14:48:20 +0100] rev 57449
avoid name clash
blanchet [Thu, 13 Mar 2014 14:48:20 +0100] rev 57448
simplify index handling
blanchet [Thu, 13 Mar 2014 14:48:20 +0100] rev 57447
more robust indices
blanchet [Thu, 13 Mar 2014 14:48:20 +0100] rev 57446
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
blanchet [Thu, 13 Mar 2014 14:48:20 +0100] rev 57445
move lemmas to theory file, towards textual proof reconstruction
blanchet [Thu, 13 Mar 2014 14:48:05 +0100] rev 57444
simpler translation of 'div' and 'mod' for Z3
blanchet [Thu, 13 Mar 2014 13:18:14 +0100] rev 57443
tuning
blanchet [Thu, 13 Mar 2014 13:18:14 +0100] rev 57442
tuning
blanchet [Thu, 13 Mar 2014 13:18:14 +0100] rev 57441
thread through step IDs from Z3 to Sledgehammer
blanchet [Thu, 13 Mar 2014 13:18:14 +0100] rev 57440
adapted to ML structure renaming