Differences

This shows you the differences between two versions of the page.

--- reference:rule_calculus [2011/06/13 22:05] – created 178.26.109.100
+++ reference:rule_calculus [2011/06/13 22:05] (current) – [In Isabelle/HOL] 178.26.109.100
@@ Line 19: / Line 19: @@
 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.