Moved rule instantiation related types to corresponding package (and gave the package a better name)

Author: unp1

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java

@@ -21,9 +21,9 @@
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
 
 import org.key_project.logic.Name;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.Rule;
 import org.key_project.prover.rules.RuleApp;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableList;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java

@@ -37,9 +37,9 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.op.SortedOperator;
 import org.key_project.logic.sort.Sort;
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.RuleApp;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.Sequent;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java

@@ -13,7 +13,7 @@
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
 import org.key_project.logic.Name;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 
 /**
  * {@link Strategy} used to simplify {@link Term}s in side proofs.

key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java

@@ -13,10 +13,10 @@
 import de.uka.ilkd.key.rule.match.vm.VMTacletMatcher;
 
 import org.key_project.logic.Name;
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
-import org.key_project.prover.rules.AssumesMatchResult;
-import org.key_project.prover.rules.inst.SVInstantiations;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesMatchResult;
+import org.key_project.prover.rules.instantiation.SVInstantiations;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableArray;

key.core/src/main/java/de/uka/ilkd/key/api/SearchNode.java

@@ -5,8 +5,8 @@
 
 import de.uka.ilkd.key.logic.Term;
 
-import org.key_project.prover.rules.MatchConditions;
-import org.key_project.prover.rules.inst.SVInstantiations;
+import org.key_project.prover.rules.instantiation.MatchConditions;
+import org.key_project.prover.rules.instantiation.SVInstantiations;
 import org.key_project.prover.sequent.SequentFormula;
 
 /**

key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java

@@ -22,8 +22,8 @@
 import de.uka.ilkd.key.strategy.FocussedBreakpointRuleApplicationManager;
 import de.uka.ilkd.key.strategy.FocussedRuleApplicationManager;
 
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;

key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletAssumesModel.java

@@ -22,8 +22,8 @@
 import de.uka.ilkd.key.util.RecognitionException;
 
 import org.key_project.logic.LogicServices;
-import org.key_project.prover.rules.AssumesFormulaInstDirect;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableList;
 

key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java

@@ -16,8 +16,8 @@
 import de.uka.ilkd.key.rule.inst.SortException;
 
 import org.key_project.logic.Namespace;
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;

key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java

@@ -13,7 +13,7 @@
 import de.uka.ilkd.key.util.properties.Properties;
 
 import org.key_project.logic.LogicServices;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.Semisequent;
 import org.key_project.prover.sequent.SequentChangeInfo;

key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java

@@ -17,8 +17,8 @@
 import de.uka.ilkd.key.rule.inst.*;
 
 import org.key_project.logic.PosInTerm;
-import org.key_project.prover.rules.inst.InstantiationEntry;
-import org.key_project.prover.rules.inst.ListInstantiation;
+import org.key_project.prover.rules.instantiation.InstantiationEntry;
+import org.key_project.prover.rules.instantiation.ListInstantiation;
 import org.key_project.prover.sequent.*;
 import org.key_project.util.collection.*;