Fixed non-escaped underscore in section headings (document generation should
authorwebertj
Mon Apr 14 13:51:31 2003 +0200 (2003-04-14)
changeset 13909a5247a49c85e
parent 13908 4bdfa9f77254
child 13910 f9a9ef16466f
Fixed non-escaped underscore in section headings (document generation should
work again now).
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Fri Apr 11 23:11:13 2003 +0200
     1.2 +++ b/src/HOL/Map.thy	Mon Apr 14 13:51:31 2003 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4          "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
     1.5  
     1.6  
     1.7 -section "empty"
     1.8 +section {* empty *}
     1.9  
    1.10  lemma empty_upd_none: "empty(x := None) = empty"
    1.11  apply (rule ext)
    1.12 @@ -69,7 +69,7 @@
    1.13  declare sum_case_empty_empty [simp]
    1.14  
    1.15  
    1.16 -section "map_upd"
    1.17 +section {* map\_upd *}
    1.18  
    1.19  lemma map_upd_triv: "t k = Some x ==> t(k|->x) = t"
    1.20  apply (rule ext)
    1.21 @@ -93,7 +93,7 @@
    1.22  
    1.23  
    1.24  (* FIXME: what is this sum_case nonsense?? *)
    1.25 -section "sum_case and empty/map_upd"
    1.26 +section {* sum\_case and empty/map\_upd *}
    1.27  
    1.28  lemma sum_case_map_upd_empty: "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
    1.29  apply (rule ext)
    1.30 @@ -114,7 +114,7 @@
    1.31  declare sum_case_map_upd_map_upd [simp]
    1.32  
    1.33  
    1.34 -section "map_upds"
    1.35 +section {* map\_upds *}
    1.36  
    1.37  lemma map_upds_twist [rule_format (no_asm)]: "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))"
    1.38  apply (induct_tac "as")
    1.39 @@ -128,7 +128,7 @@
    1.40  declare map_upds_twist [simp]
    1.41  
    1.42  
    1.43 -section "chg_map"
    1.44 +section {* chg\_map *}
    1.45  
    1.46  lemma chg_map_new: "m a = None   ==> chg_map f a m = m"
    1.47  apply (unfold chg_map_def)
    1.48 @@ -143,7 +143,7 @@
    1.49  declare chg_map_new [simp] chg_map_upd [simp]
    1.50  
    1.51  
    1.52 -section "map_of"
    1.53 +section {* map\_of *}
    1.54  
    1.55  lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
    1.56  apply (induct_tac "xs")
    1.57 @@ -184,7 +184,7 @@
    1.58  done
    1.59  
    1.60  
    1.61 -section "option_map related"
    1.62 +section {* option\_map related *}
    1.63  
    1.64  lemma option_map_o_empty: "option_map f o empty = empty"
    1.65  apply (rule ext)
    1.66 @@ -199,7 +199,7 @@
    1.67  declare option_map_o_empty [simp] option_map_o_map_upd [simp]
    1.68  
    1.69  
    1.70 -section "++"
    1.71 +section {* ++ *}
    1.72  
    1.73  lemma override_empty: "m ++ empty = m"
    1.74  apply (unfold override_def)
    1.75 @@ -261,7 +261,7 @@
    1.76  declare fun_upd_apply [simp]
    1.77  
    1.78  
    1.79 -section "dom"
    1.80 +section {* dom *}
    1.81  
    1.82  lemma domI: "m a = Some b ==> a : dom m"
    1.83  apply (unfold dom_def)
    1.84 @@ -305,7 +305,7 @@
    1.85  done
    1.86  declare dom_override [simp]
    1.87  
    1.88 -section "ran"
    1.89 +section {* ran *}
    1.90  
    1.91  lemma ran_empty: "ran empty = {}"
    1.92  apply (unfold ran_def)