User Tools
reference:rule_calculus
Differences
This shows you the differences between two versions of the page.
|
reference:rule_calculus [2011/06/13 22:05] 178.26.109.100 created |
reference:rule_calculus [2011/06/13 22:05] (current) 178.26.109.100 [In Isabelle/HOL] |
||
|---|---|---|---|
| Line 19: | Line 19: | ||
| which is equivalent to above definition. | which is equivalent to above definition. | ||
| - | The nice things about Isabelle/HOL is that you can use your own theorems as rules if they have this format. You can tell Isabelle to transform a theorem into this form (if possible) by using the ''[[[rule_format]]]'' directive. | + | The nice things about Isabelle/HOL is that you can use your own theorems as rules if they have this format. You can tell Isabelle to transform a theorem into this form (if possible) by using the ''[[rule_format]]'' directive. |
reference/rule_calculus.1307995514.txt.gz ยท Last modified: 2011/06/13 22:05 by 178.26.109.100
Page Tools
