Uses of Package
net.sourceforge.czt.zeves.ast

Packages that use net.sourceforge.czt.zeves.ast

Package	Description
net.sourceforge.czt.zeves.ast	Interfaces of the AST for ZEves.
net.sourceforge.czt.zeves.impl	Implementation classes of the AST for ZEves.
net.sourceforge.czt.zeves.jaxb	Provides classes enabling validation as well as reading and writing XML using Jaxb generated classes.
net.sourceforge.czt.zeves.util
net.sourceforge.czt.zeves.visitor	Visitors for the AST for ZEves.

Classes in net.sourceforge.czt.zeves.ast used by net.sourceforge.czt.zeves.ast

Class and Description
ApplyCommand Theorem application commands.
CaseAnalysisCommand Goal splitting and case analysis commands.
CaseAnalysisKind A(n) CaseAnalysisKind enumeration.
ComplexCommand Abstract complex command.
Instantiation Encapsulates one instantiation or replacement for the instantiate or use commands.
InstantiationCommand Abstract command for instantiations.
InstantiationKind A(n) InstantiationKind enumeration.
InstantiationList List of possible instantiations.
LabelAbility A(n) LabelAbility enumeration.
LabelUsage A(n) LabelUsage enumeration.
NormalizationCommand Term rewriting via normal forms.
NormalizationKind A(n) NormalizationKind enumeration.
ProofCommand Abstract proof command
ProofCommandInfo
ProofCommandInfoList
ProofCommandList
ProofScript Sequence of proof commands
ProofStepKind A(n) ProofStepKind enumeration.
ProofStepScope A(n) ProofStepScope enumeration.
ProofType Proof command information collected to form a proof script type.
QuantifiersCommand Quantifier manipulation and elimination.
RewriteKind A(n) RewriteKind enumeration.
RewritePower A(n) RewritePower enumeration.
SimplificationCommand Term rewriting and simplification commands of various kinds.
SorryCommand Sorry and Oops - virtual - commands; inspired by Isabelle's meanings: sorry is give up on proving, yet keep the theorem; oops, gives up on proving, but don't keep the theorem albeit leave the goal.
SubstitutionCommand Term substitution commands.
SubstitutionKind A(n) SubstitutionKind enumeration.
UseCommand Theorem / axiom introduction with particular parameters / instantiations.
WithCommand Compound commands involving either specific theorem names and/or expressions/predicates.
WrappedCommand Abstract proof command that wraps up another proof command within it.
ZEvesLabel Label to theorems and axiomatic predicates
ZEvesNote Notes and comments from the user within formal text (not type checked)

Classes in net.sourceforge.czt.zeves.ast used by net.sourceforge.czt.zeves.impl

Class and Description
ApplyCommand Theorem application commands.
CaseAnalysisCommand Goal splitting and case analysis commands.
CaseAnalysisKind A(n) CaseAnalysisKind enumeration.
ComplexCommand Abstract complex command.
Instantiation Encapsulates one instantiation or replacement for the instantiate or use commands.
InstantiationCommand Abstract command for instantiations.
InstantiationKind A(n) InstantiationKind enumeration.
InstantiationList List of possible instantiations.
LabelAbility A(n) LabelAbility enumeration.
LabelUsage A(n) LabelUsage enumeration.
NormalizationCommand Term rewriting via normal forms.
NormalizationKind A(n) NormalizationKind enumeration.
ProofCommand Abstract proof command
ProofCommandInfo
ProofCommandInfoList
ProofCommandList
ProofScript Sequence of proof commands
ProofStepKind A(n) ProofStepKind enumeration.
ProofStepScope A(n) ProofStepScope enumeration.
ProofType Proof command information collected to form a proof script type.
QuantifiersCommand Quantifier manipulation and elimination.
RewriteKind A(n) RewriteKind enumeration.
RewritePower A(n) RewritePower enumeration.
SimplificationCommand Term rewriting and simplification commands of various kinds.
SorryCommand Sorry and Oops - virtual - commands; inspired by Isabelle's meanings: sorry is give up on proving, yet keep the theorem; oops, gives up on proving, but don't keep the theorem albeit leave the goal.
SubstitutionCommand Term substitution commands.
SubstitutionKind A(n) SubstitutionKind enumeration.
UseCommand Theorem / axiom introduction with particular parameters / instantiations.
WithCommand Compound commands involving either specific theorem names and/or expressions/predicates.
WrappedCommand Abstract proof command that wraps up another proof command within it.
ZEvesFactory The object factory for the AST.
ZEvesLabel Label to theorems and axiomatic predicates
ZEvesNote Notes and comments from the user within formal text (not type checked)

Classes in net.sourceforge.czt.zeves.ast used by net.sourceforge.czt.zeves.jaxb

Class and Description
ApplyCommand Theorem application commands.
CaseAnalysisCommand Goal splitting and case analysis commands.
Instantiation Encapsulates one instantiation or replacement for the instantiate or use commands.
InstantiationList List of possible instantiations.
NormalizationCommand Term rewriting via normal forms.
ProofCommandInfo
ProofCommandInfoList
ProofCommandList
ProofScript Sequence of proof commands
ProofType Proof command information collected to form a proof script type.
QuantifiersCommand Quantifier manipulation and elimination.
SimplificationCommand Term rewriting and simplification commands of various kinds.
SorryCommand Sorry and Oops - virtual - commands; inspired by Isabelle's meanings: sorry is give up on proving, yet keep the theorem; oops, gives up on proving, but don't keep the theorem albeit leave the goal.
SubstitutionCommand Term substitution commands.
UseCommand Theorem / axiom introduction with particular parameters / instantiations.
WithCommand Compound commands involving either specific theorem names and/or expressions/predicates.
ZEvesFactory The object factory for the AST.
ZEvesLabel Label to theorems and axiomatic predicates
ZEvesNote Notes and comments from the user within formal text (not type checked)

Classes in net.sourceforge.czt.zeves.ast used by net.sourceforge.czt.zeves.util

Class and Description
ApplyCommand Theorem application commands.
CaseAnalysisCommand Goal splitting and case analysis commands.
CaseAnalysisKind A(n) CaseAnalysisKind enumeration.
Instantiation Encapsulates one instantiation or replacement for the instantiate or use commands.
InstantiationKind A(n) InstantiationKind enumeration.
InstantiationList List of possible instantiations.
LabelAbility A(n) LabelAbility enumeration.
LabelUsage A(n) LabelUsage enumeration.
NormalizationCommand Term rewriting via normal forms.
NormalizationKind A(n) NormalizationKind enumeration.
ProofCommand Abstract proof command
ProofCommandInfo
ProofCommandInfoList
ProofCommandList
ProofScript Sequence of proof commands
ProofStepKind A(n) ProofStepKind enumeration.
ProofStepScope A(n) ProofStepScope enumeration.
ProofType Proof command information collected to form a proof script type.
QuantifiersCommand Quantifier manipulation and elimination.
RewriteKind A(n) RewriteKind enumeration.
RewritePower A(n) RewritePower enumeration.
SimplificationCommand Term rewriting and simplification commands of various kinds.
SorryCommand Sorry and Oops - virtual - commands; inspired by Isabelle's meanings: sorry is give up on proving, yet keep the theorem; oops, gives up on proving, but don't keep the theorem albeit leave the goal.
SubstitutionCommand Term substitution commands.
SubstitutionKind A(n) SubstitutionKind enumeration.
UseCommand Theorem / axiom introduction with particular parameters / instantiations.
WithCommand Compound commands involving either specific theorem names and/or expressions/predicates.
ZEvesFactory The object factory for the AST.
ZEvesLabel Label to theorems and axiomatic predicates
ZEvesNote Notes and comments from the user within formal text (not type checked)

Classes in net.sourceforge.czt.zeves.ast used by net.sourceforge.czt.zeves.visitor

Class and Description
ApplyCommand Theorem application commands.
CaseAnalysisCommand Goal splitting and case analysis commands.
ComplexCommand Abstract complex command.
Instantiation Encapsulates one instantiation or replacement for the instantiate or use commands.
InstantiationCommand Abstract command for instantiations.
InstantiationList List of possible instantiations.
NormalizationCommand Term rewriting via normal forms.
ProofCommand Abstract proof command
ProofCommandInfo
ProofCommandInfoList
ProofCommandList
ProofScript Sequence of proof commands
ProofType Proof command information collected to form a proof script type.
QuantifiersCommand Quantifier manipulation and elimination.
SimplificationCommand Term rewriting and simplification commands of various kinds.
SorryCommand Sorry and Oops - virtual - commands; inspired by Isabelle's meanings: sorry is give up on proving, yet keep the theorem; oops, gives up on proving, but don't keep the theorem albeit leave the goal.
SubstitutionCommand Term substitution commands.
UseCommand Theorem / axiom introduction with particular parameters / instantiations.
WithCommand Compound commands involving either specific theorem names and/or expressions/predicates.
WrappedCommand Abstract proof command that wraps up another proof command within it.
ZEvesLabel Label to theorems and axiomatic predicates
ZEvesNote Notes and comments from the user within formal text (not type checked)