equal
deleted
inserted
replaced
8 notation (latex output) |
8 notation (latex output) |
9 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and |
9 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and |
10 Seq (infixr "\<cdot>" 100) and |
10 Seq (infixr "\<cdot>" 100) and |
11 Star ("_\<^bsup>\<star>\<^esup>") and |
11 Star ("_\<^bsup>\<star>\<^esup>") and |
12 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and |
12 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and |
13 Suc ("_+1" [100] 100) |
13 Suc ("_+1" [100] 100) and |
|
14 quotient ("_ \<^raw:\ensuremath{\sslash}> _ " [90, 90] 90) |
|
15 |
14 |
16 |
15 (*>*) |
17 (*>*) |
16 |
18 |
17 section {* Introduction *} |
19 section {* Introduction *} |
18 |
20 |