Opened 17 years ago
Last modified 11 years ago
#95 new defect
Refine spuriouscmd into two: destructivecmd and diagnosticcmd
Reported by: | David Aspinall | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | |
Component: | 4:prover-isabelle | Keywords: | |
Cc: |
Description
Makarius notes that spuriouscmd cannot be pruned from scripts because we classify
use_thy
and ML
and they may change state.
Perhaps we should split these into two things?
Needs an extra kind in Isar.
Note: See
TracTickets for help on using
tickets.
Milestone PG-Eclipse-1.1.0 deleted