src/HOL/Library/Transitive_Closure_Table.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60519 84b8e5c2580e
     1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
     1.5  
     1.6 -section {* A table-based implementation of the reflexive transitive closure *}
     1.7 +section \<open>A table-based implementation of the reflexive transitive closure\<close>
     1.8  
     1.9  theory Transitive_Closure_Table
    1.10  imports Main
    1.11 @@ -22,9 +22,9 @@
    1.12      then show ?case ..
    1.13    next
    1.14      case (step x z)
    1.15 -    from `\<exists>xs. rtrancl_path r z xs y`
    1.16 +    from \<open>\<exists>xs. rtrancl_path r z xs y\<close>
    1.17      obtain xs where "rtrancl_path r z xs y" ..
    1.18 -    with `r x z` have "rtrancl_path r x (z # xs) y"
    1.19 +    with \<open>r x z\<close> have "rtrancl_path r x (z # xs) y"
    1.20        by (rule rtrancl_path.step)
    1.21      then show ?case ..
    1.22    qed
    1.23 @@ -37,7 +37,7 @@
    1.24      show ?case by (rule rtranclp.rtrancl_refl)
    1.25    next
    1.26      case (step x y ys z)
    1.27 -    from `r x y` `r\<^sup>*\<^sup>* y z` show ?case
    1.28 +    from \<open>r x y\<close> \<open>r\<^sup>*\<^sup>* y z\<close> show ?case
    1.29        by (rule converse_rtranclp_into_rtranclp)
    1.30    qed
    1.31  qed
    1.32 @@ -53,7 +53,7 @@
    1.33    case (step x y xs)
    1.34    then have "rtrancl_path r y (xs @ ys) z"
    1.35      by simp
    1.36 -  with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z"
    1.37 +  with \<open>r x y\<close> have "rtrancl_path r x (y # (xs @ ys)) z"
    1.38      by (rule rtrancl_path.step)
    1.39    then show ?case by simp
    1.40  qed
    1.41 @@ -83,7 +83,7 @@
    1.42        by (rule rtrancl_path.step)
    1.43      then have "rtrancl_path r x ((a # as) @ [y]) y"
    1.44        by simp
    1.45 -    then show ?thesis using `rtrancl_path r y ys z`
    1.46 +    then show ?thesis using \<open>rtrancl_path r y ys z\<close>
    1.47        by (rule Cons(2))
    1.48    qed
    1.49  qed
    1.50 @@ -96,7 +96,7 @@
    1.51    show ?case
    1.52    proof (cases "distinct (x # xs)")
    1.53      case True
    1.54 -    with `rtrancl_path r x xs y` show ?thesis by (rule less)
    1.55 +    with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less)
    1.56    next
    1.57      case False
    1.58      then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
    1.59 @@ -108,7 +108,7 @@
    1.60        case Nil
    1.61        with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
    1.62          by auto
    1.63 -      from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
    1.64 +      from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y"
    1.65          by (auto elim: rtrancl_path_appendE)
    1.66        from xs have "length cs < length xs" by simp
    1.67        then show ?thesis
    1.68 @@ -117,7 +117,7 @@
    1.69        case (Cons d ds)
    1.70        with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
    1.71          by auto
    1.72 -      with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
    1.73 +      with \<open>rtrancl_path r x xs y\<close> obtain xa: "rtrancl_path r x (ds @ [a]) a"
    1.74          and ay: "rtrancl_path r a (bs @ a # cs) y"
    1.75          by (auto elim: rtrancl_path_appendE)
    1.76        from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
    1.77 @@ -152,7 +152,7 @@
    1.78      by auto
    1.79    ultimately have "rtrancl_tab r (x # ys) y z"
    1.80      by (rule step)
    1.81 -  with `x \<notin> set ys` `r x y`
    1.82 +  with \<open>x \<notin> set ys\<close> \<open>r x y\<close>
    1.83    show ?case by (rule rtrancl_tab.step)
    1.84  qed
    1.85