mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 00:55:31 +00:00
Fix typos.
This commit is contained in:
parent
44b2c3ce6b
commit
4bc1b0b8c8
5 changed files with 5 additions and 5 deletions
|
@ -253,7 +253,7 @@ namespace qe {
|
|||
/**
|
||||
\brief Guarded definitions.
|
||||
|
||||
A realizer to a an existential quantified formula is a disjunction
|
||||
A realizer to an existential quantified formula is a disjunction
|
||||
together with a substitution from the existentially quantified variables
|
||||
to terms such that:
|
||||
1. The original formula (exists (vars) fml) is equivalent to the disjunction of guards.
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue