standardRules.key
Requires: \includeldt;
requires ldt
Requires: \include"./classicalLogic/propRule.key";
requires "./classicalLogic/propRule.key"
Requires: \include"./classicalLogic/firstOrderRules.key";
requires "./classicalLogic/firstOrderRules.key"
Requires: \includeifThenElseRules;
requires ifThenElseRules
Requires: \include"./classicalLogic/formulaNormalisationRules.key";
requires "./classicalLogic/formulaNormalisationRules.key"
Requires: \includeupdateRules;
requires updateRules
Requires: \include"./integer/integerRulesCommon.key";
requires "./integer/integerRulesCommon.key"
Requires: \include"./integer/intRules.key","./integer/intRulesUncheckedSemantics.key","./integer/intRulesCheckedSemantics.key","./integer/intRulesJavaSemantics.key";
requires "./integer/intRules.key"
requires "./integer/intRulesUncheckedSemantics.key"
requires "./integer/intRulesCheckedSemantics.key"
requires "./integer/intRulesJavaSemantics.key"
Requires: \include"./integer/integerSimplificationRules.key";
requires "./integer/integerSimplificationRules.key"
Requires: \include"./integer/intDiv.key";
requires "./integer/intDiv.key"
Requires: \include"./integer/bsum.key","./integer/bprod.key";
requires "./integer/bsum.key"
requires "./integer/bprod.key"
Requires: \include"./integer/binaryAxioms.key","./integer/binaryLemmas.key";
requires "./integer/binaryAxioms.key"
requires "./integer/binaryLemmas.key"
Requires: \include"./integer/intPow.key";
requires "./integer/intPow.key"
Requires: \include"./float/floatRulesCommon.key";
requires "./float/floatRulesCommon.key"
Requires: \include"./float/floatRules.key","./float/floatRulesVerifyNormal.key","./float/floatRulesAssumeStrictfp.key";
requires "./float/floatRules.key"
requires "./float/floatRulesVerifyNormal.key"
requires "./float/floatRulesAssumeStrictfp.key"
Requires: \includegenericRules;
requires genericRules
Requires: \includebooleanRules;
requires booleanRules
Requires: \includeepsilon;
requires epsilon
Requires: \include"./locset/locSetsRules.key";
requires "./locset/locSetsRules.key"
Requires: \includeheapRules;
requires heapRules
Requires: \include"./permission/permissionRules.key";
requires "./permission/permissionRules.key"
Requires: \includereachRules;
requires reachRules
Requires: \include"./sequence/seqCoreRules.key","./sequence/seqRules.key";
requires "./sequence/seqCoreRules.key"
requires "./sequence/seqRules.key"
Requires: \include"./sequence/seqPerm.key";
requires "./sequence/seqPerm.key"
Requires: \include"./sequence/seqPerm2.key";
requires "./sequence/seqPerm2.key"
Requires: \includejavaRules;
requires javaRules
Requires: \includeloopRules;
requires loopRules
Requires: \includeactiveUse;
requires activeUse
Requires: \includeinstanceAllocation;
requires instanceAllocation
Requires: \includejava5;
requires java5
Requires: \include"./integer/integerAssignment2UpdateRules.key";
requires "./integer/integerAssignment2UpdateRules.key"
Requires: \include"./float/floatAssignment2UpdateRules.key";
requires "./float/floatAssignment2UpdateRules.key"
Requires: \include"./integer/bigint.key";
requires "./integer/bigint.key"
Requires: \includeadtProgramDecompositionRules;
requires adtProgramDecompositionRules
Requires: \includeprecRules;
requires precRules
Requires: \includeString;
requires String
Requires: \include"./string/charListRules.key";
requires "./string/charListRules.key"
Requires: \include"./string/regExTheory.key";
requires "./string/regExTheory.key"
Requires: \include"./sequence/seqEq.key";
requires "./sequence/seqEq.key"
Requires: \includeinfFlow;
requires infFlow
Requires: \includemapSize;
requires mapSize
Requires: \includeloopInvariantRules;
requires loopInvariantRules
Requires: \includeforLoopRules;
requires forLoopRules
Requires: \includeexecRules;
requires execRules
Requires: \includeloopScopeRules;
requires loopScopeRules