14 |
14 |
15 |
15 |
16 declare [[show_question_marks = false]] |
16 declare [[show_question_marks = false]] |
17 |
17 |
18 syntax (latex output) |
18 syntax (latex output) |
19 "_Collect" :: "pttrn => bool => 'a set" ("(1{_ \<^raw:\mbox{\boldmath$\mid$}> _})") |
19 "_Collect" :: "pttrn => bool => 'a set" ("(1{_ \<^latex>\<open>\\mbox{\\boldmath$\\mid$}\<close> _})") |
20 "_CollectIn" :: "pttrn => 'a set => bool => 'a set" ("(1{_ \<in> _ |e _})") |
20 "_CollectIn" :: "pttrn => 'a set => bool => 'a set" ("(1{_ \<in> _ |e _})") |
21 |
21 |
22 syntax |
22 syntax |
23 "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>_.a./ _)" [0, 10] 10) |
23 "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>_.a./ _)" [0, 10] 10) |
24 "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>!_.a./ _)" [0, 10] 10) |
24 "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>!_.a./ _)" [0, 10] 10) |
36 |
36 |
37 |
37 |
38 |
38 |
39 |
39 |
40 notation (latex output) |
40 notation (latex output) |
41 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
41 If ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and |
42 Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and |
42 Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) and |
43 |
43 |
44 ZERO ("\<^bold>0" 81) and |
44 ZERO ("\<^bold>0" 81) and |
45 ONE ("\<^bold>1" 81) and |
45 ONE ("\<^bold>1" 81) and |
46 CHAR ("_" [1000] 80) and |
46 CHAR ("_" [1000] 80) and |
47 ALT ("_ + _" [77,77] 78) and |
47 ALT ("_ + _" [77,77] 78) and |
80 F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and |
80 F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and |
81 simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and |
81 simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and |
82 simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and |
82 simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and |
83 slexer ("lexer\<^sup>+" 1000) and |
83 slexer ("lexer\<^sup>+" 1000) and |
84 |
84 |
85 at ("_\<^raw:\mbox{$\downharpoonleft$}>\<^bsub>_\<^esub>") and |
85 at ("_\<^latex>\<open>\\mbox{$\\downharpoonleft$}\<close>\<^bsub>_\<^esub>") and |
86 lex_list ("_ \<prec>\<^bsub>lex\<^esub> _") and |
86 lex_list ("_ \<prec>\<^bsub>lex\<^esub> _") and |
87 PosOrd ("_ \<prec>\<^bsub>_\<^esub> _" [77,77,77] 77) and |
87 PosOrd ("_ \<prec>\<^bsub>_\<^esub> _" [77,77,77] 77) and |
88 PosOrd_ex ("_ \<prec> _" [77,77] 77) and |
88 PosOrd_ex ("_ \<prec> _" [77,77] 77) and |
89 PosOrd_ex_eq ("_ \<^raw:\mbox{$\preccurlyeq$}> _" [77,77] 77) and |
89 PosOrd_ex_eq ("_ \<^latex>\<open>\\mbox{$\\preccurlyeq$}\<close> _" [77,77] 77) and |
90 pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and |
90 pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and |
91 nprec ("_ \<^raw:\mbox{$\not\prec$}> _" [77,77] 77) and |
91 nprec ("_ \<^latex>\<open>\\mbox{$\\not\\prec$}\<close> _" [77,77] 77) and |
92 |
92 |
93 DUMMY ("\<^raw:\underline{\hspace{2mm}}>") |
93 DUMMY ("\<^latex>\<open>\\underline{\\hspace{2mm}}\<close>") |
94 |
94 |
95 |
95 |
96 definition |
96 definition |
97 "match r s \<equiv> nullable (ders s r)" |
97 "match r s \<equiv> nullable (ders s r)" |
98 |
98 |