equal
deleted
inserted
replaced
92 \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x) |
92 \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x) |
93 |
93 |
94 * The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@" |
94 * The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@" |
95 has been removed for output. It is retained for input only, until it is |
95 has been removed for output. It is retained for input only, until it is |
96 eliminated altogether. |
96 eliminated altogether. |
|
97 |
|
98 * Sledgehammer: |
|
99 - Produce syntactically correct Vampire 4.0 problem files. |
97 |
100 |
98 * (Co)datatype package: |
101 * (Co)datatype package: |
99 - New commands for defining corecursive functions and reasoning about |
102 - New commands for defining corecursive functions and reasoning about |
100 them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive', |
103 them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive', |
101 'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof |
104 'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof |