diff options
| -rw-r--r-- | spartan/theories/Identity.thy | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy index 1ab12ff..01bea46 100644 --- a/spartan/theories/Identity.thy +++ b/spartan/theories/Identity.thy @@ -139,18 +139,9 @@ in val _ = Context.>> end \<close> -text \<open>Set up \<open>sym\<close> attribute for propositional equalities:\<close> - -ML \<open> -structure Id_Sym_Attr = Sym_Attr ( - struct - val name = "sym" - val symmetry_rule = @{thm pathinv[rotated 3]} - end -) -\<close> - -setup \<open>Id_Sym_Attr.setup\<close> +lemmas + [sym] = pathinv[rotated 3] and + [trans] = pathcomp[rotated 4] section \<open>Basic propositional equalities\<close> |