Tue, 06 Nov 2012 11:20:56 +0100 | blanchet | correct parsing of E dependencies | changeset | files |
Tue, 06 Nov 2012 11:20:56 +0100 | blanchet | proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction | changeset | files |
Mon, 05 Nov 2012 11:40:51 +0100 | nipkow | tuned | changeset | files |
Sun, 04 Nov 2012 18:41:27 +0100 | nipkow | code for while directly, not via while_option | changeset | files |
Sun, 04 Nov 2012 18:38:18 +0100 | nipkow | executable true liveness analysis incl an approximating version | changeset | files |
Sun, 04 Nov 2012 17:36:26 +0100 | nipkow | now that sets are executable again, no more special treatment of variable sets | changeset | files |