diff options
| author | Josh Chen | 2020-05-25 16:01:18 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-25 16:01:18 +0200 |
| commit | 575e98cac4871f0fdeefa0f5ac75bbba8103e82e (patch) | |
| tree | 02c4ed672816f36475408b99bab5ba0fa4f0cd26 /spartan/theories | |
| parent | 8f47d9f3ca38a3fc2c3c462d1157866081102ce1 (diff) | |
use existing calculation infrastructure for sym and trans
Diffstat (limited to 'spartan/theories')
| -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> |