isabelle: Changelog

blanchet [Tue, 18 Feb 2014 17:52:28 +0100] rev 55567

tuning

blanchet [Tue, 18 Feb 2014 17:52:27 +0100] rev 55566

made SML/NJ happier

kuncar [Tue, 18 Feb 2014 23:03:50 +0100] rev 55565

simplify proofs because of the stronger reflexivity prover

kuncar [Tue, 18 Feb 2014 23:03:49 +0100] rev 55564

delete or move now not necessary reflexivity rules due to 1726f46d2aa8

kuncar [Tue, 18 Feb 2014 23:03:47 +0100] rev 55563

implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules

wenzelm [Tue, 18 Feb 2014 21:00:13 +0100] rev 55562

merged

wenzelm [Tue, 18 Feb 2014 20:50:07 +0100] rev 55561

more markup;

wenzelm [Tue, 18 Feb 2014 20:37:45 +0100] rev 55560

proper term equality; proper Args.term_pattern parser (like 'is' or 'let' in Isar);

isabelle