2012-11-12 blanchet fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
2012-11-12 blanchet create temp directory if not already created
2012-11-12 nipkow merged
2012-11-12 nipkow new theory IMP/Finite_Reachable
2012-11-12 blanchet avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
2012-11-12 blanchet centralized term printing code
2012-11-12 blanchet thread context correctly when printing backquoted facts
2012-11-11 haftmann dropped dead code;
2012-11-11 haftmann modernized, simplified and compacted oracle and proof method glue code;
2012-11-09 nipkow merged
2012-11-09 nipkow fixed underscores
2012-11-09 immler moved lemmas into projective_family; added header for theory Projective_Family
Loading...
(0) -30000 -10000 -3000 -1000 -300 -100 -12 +12 +100 +300 +1000 +3000 +10000 +30000 tip