nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Update Attributes examples

This commit is contained in:
Nicolas Méric 2022-12-09 15:12:38 +01:00
parent 8cee80d78e
commit 312734afbd
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/tests/Attributes.thy
View File

@ -204,10 +204,10 @@ value*\<open>(map fst @{trace-attribute \<open>aaa\<close>}) \<close>
definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*"
value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>
definition word_test :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> bool" (infix "is\<^sub>\<longrightarrow>in" 60)
where " w is\<^sub>\<longrightarrow>in rexp \<equiv> DA.accepts (na2da (rexp2na rexp)) (w)"
definition word_test :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> bool" (infix "is-in" 60)
where " w is-in rexp \<equiv> DA.accepts (na2da (rexp2na rexp)) (w)"
value* \<open> (map fst @{trace-attribute \<open>aaa\<close>}) is\<^sub>\<longrightarrow>in example_expression \<close>
value* \<open> (map fst @{trace-attribute \<open>aaa\<close>}) is-in example_expression \<close>
(*<*)