blanchet [Tue, 18 Feb 2014 23:08:55 +0100] rev 56910
merged
blanchet [Tue, 18 Feb 2014 17:52:28 +0100] rev 56909
tuning
blanchet [Tue, 18 Feb 2014 17:52:27 +0100] rev 56908
made SML/NJ happier
kuncar [Tue, 18 Feb 2014 23:03:50 +0100] rev 56907
simplify proofs because of the stronger reflexivity prover
kuncar [Tue, 18 Feb 2014 23:03:49 +0100] rev 56906
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
kuncar [Tue, 18 Feb 2014 23:03:47 +0100] rev 56905
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 56904
merged
wenzelm [Tue, 18 Feb 2014 20:50:07 +0100] rev 56903
more markup;
wenzelm [Tue, 18 Feb 2014 20:37:45 +0100] rev 56902
proper term equality;
proper Args.term_pattern parser (like 'is' or 'let' in Isar);
wenzelm [Tue, 18 Feb 2014 20:32:58 +0100] rev 56901
tuned message;