| changeset 62020 | 5d208fd2507d |
| parent 60770 | 240563fbf41d |
| child 62143 | 3c9a0985e6be |
--- a/src/CCL/Term.thy Thu Dec 31 21:46:31 2015 +0100 +++ b/src/CCL/Term.thy Fri Jan 01 10:49:00 2016 +0100 @@ -291,7 +291,7 @@ \<close> -subsection \<open>Rules for pre-order @{text "[="}\<close> +subsection \<open>Rules for pre-order \<open>[=\<close>\<close> lemma term_porews: "inl(a) [= inl(a') \<longleftrightarrow> a [= a'"