Changeset 11878

Timestamp:

06.07.2009 10:30:10 (5 months ago)

Author:

mgross

Message:

First version of the conservativity rules (incomplete)

Location:

trunk

Files:

• Interfaces/CmdAction.hs (modified) (2 diffs)
• Interfaces/Command.hs (modified) (3 diffs)
• Proofs/Conservativity.hs (added)

trunk/Interfaces/CmdAction.hs

@@ -23 +23 @@
 import Proofs.HideTheoremShift (automaticHideTheoremShift)
 import Proofs.TheoremHideShift (theoremHideShift)
+import Proofs.Conservativity (conservativity)
 import Proofs.ComputeColimit (computeColimit)
 
@@ -41 +42 @@
   , (CompositionProveEdges, composition)
   , (CompositionCreateEdges, compositionCreatingEdges)
+  , (Conservativity, conservativity)
   , (HideThmShift, automaticHideTheoremShift) ]
 

trunk/Interfaces/Command.hs

@@ -28 +28 @@
   | CompositionProveEdges
   | CompositionCreateEdges
+  | Conservativity
   | ThmHideShift
   | HideThmShift
@@ -57 +58 @@
   CompositionProveEdges -> "Prove composed edges"
   CompositionCreateEdges -> "Create composed proven edges"
+  Conservativity -> "Conservativity"
   ThmHideShift -> "Theorem-Hide-Shift"
   HideThmShift -> "Hide-Theorem-Shift"
@@ -82 +84 @@
   CompositionProveEdges -> "comp"
   CompositionCreateEdges -> "comp-new"
+  Conservativity -> "cons"
   ThmHideShift -> "thm-hide"
   HideThmShift -> "hide-thm"