Tue, 18 Feb 2014 17:52:28 +0100 tuning
blanchet [Tue, 18 Feb 2014 17:52:28 +0100] rev 55567
tuning
Tue, 18 Feb 2014 17:52:27 +0100 made SML/NJ happier
blanchet [Tue, 18 Feb 2014 17:52:27 +0100] rev 55566
made SML/NJ happier
Tue, 18 Feb 2014 23:03:50 +0100 simplify proofs because of the stronger reflexivity prover
kuncar [Tue, 18 Feb 2014 23:03:50 +0100] rev 55565
simplify proofs because of the stronger reflexivity prover
Tue, 18 Feb 2014 23:03:49 +0100 delete or move now not necessary reflexivity rules due to 1726f46d2aa8
kuncar [Tue, 18 Feb 2014 23:03:49 +0100] rev 55564
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
Tue, 18 Feb 2014 23:03:47 +0100 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
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
Tue, 18 Feb 2014 21:00:13 +0100 merged
wenzelm [Tue, 18 Feb 2014 21:00:13 +0100] rev 55562
merged
Tue, 18 Feb 2014 20:50:07 +0100 more markup;
wenzelm [Tue, 18 Feb 2014 20:50:07 +0100] rev 55561
more markup;
Tue, 18 Feb 2014 20:37:45 +0100 proper term equality;
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);
Tue, 18 Feb 2014 20:32:58 +0100 tuned message;
wenzelm [Tue, 18 Feb 2014 20:32:58 +0100] rev 55559
tuned message;
Tue, 18 Feb 2014 20:20:42 +0100 more uniform treatment of dockables and their standard actions;
wenzelm [Tue, 18 Feb 2014 20:20:42 +0100] rev 55558
more uniform treatment of dockables and their standard actions;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip