equal
deleted
inserted
replaced
25 term into a propositional formula. Let |
25 term into a propositional formula. Let |
26 us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. |
26 us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. |
27 The function will return a propositional formula and a table. Suppose |
27 The function will return a propositional formula and a table. Suppose |
28 *} |
28 *} |
29 |
29 |
30 ML{*val (pform, table) = |
30 ML %grayML{*val (pform, table) = |
31 Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty*} |
31 Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty*} |
32 |
32 |
33 text {* |
33 text {* |
34 then the resulting propositional formula @{ML pform} is |
34 then the resulting propositional formula @{ML pform} is |
35 |
35 |
49 An index is also produced whenever the translation |
49 An index is also produced whenever the translation |
50 function cannot find an appropriate propositional formula for a term. |
50 function cannot find an appropriate propositional formula for a term. |
51 Attempting to translate @{term "\<forall>x::nat. P x"} |
51 Attempting to translate @{term "\<forall>x::nat. P x"} |
52 *} |
52 *} |
53 |
53 |
54 ML{*val (pform', table') = |
54 ML %grayML{*val (pform', table') = |
55 Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty*} |
55 Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty*} |
56 |
56 |
57 text {* |
57 text {* |
58 returns @{ML "BoolVar 1" in Prop_Logic} for @{ML pform'} and the table |
58 returns @{ML "BoolVar 1" in Prop_Logic} for @{ML pform'} and the table |
59 @{ML table'} is: |
59 @{ML table'} is: |