Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more antiquotations;
authorwenzelm
Sun, 12 Sep 2021 20:11:20 +0200
changeset 74299 16e5870fe21e
parent 74298 45a77ee63e57
child 74300 33f13d2d211c
more antiquotations;
src/CTT/CTT.thy file | annotate | diff | comparison | revisions 
--- a/src/CTT/CTT.thy	Sun Sep 12 20:09:36 2021 +0200
+++ b/src/CTT/CTT.thy	Sun Sep 12 20:11:20 2021 +0200
@@ -304,9 +304,9 @@
 ML \<open>
 local
 
-fun is_rigid_elem (Const(\<^const_name>\<open>Elem\<close>,_) $ a $ _) = not(is_Var (head_of a))
-  | is_rigid_elem (Const(\<^const_name>\<open>Eqelem\<close>,_) $ a $ _ $ _) = not(is_Var (head_of a))
-  | is_rigid_elem (Const(\<^const_name>\<open>Type\<close>,_) $ a) = not(is_Var (head_of a))
+fun is_rigid_elem \<^Const_>\<open>Elem for a _\<close> = not(is_Var (head_of a))
+  | is_rigid_elem \<^Const_>\<open>Eqelem for a _ _\<close> = not(is_Var (head_of a))
+  | is_rigid_elem \<^Const_>\<open>Type for a\<close> = not(is_Var (head_of a))
   | is_rigid_elem _ = false
 
 in
isabelle