src/HOL/ex/Sorting_Algorithms_Examples.thy
changeset 69597 ff784d5a5bfb
parent 69252 fc359b60121c
     1.1 --- a/src/HOL/ex/Sorting_Algorithms_Examples.thy	Sat Jan 05 17:00:43 2019 +0100
     1.2 +++ b/src/HOL/ex/Sorting_Algorithms_Examples.thy	Sat Jan 05 17:24:33 2019 +0100
     1.3 @@ -20,14 +20,14 @@
     1.4  ML \<open>
     1.5  local
     1.6  
     1.7 -  val term_of_int_list = HOLogic.mk_list @{typ int}
     1.8 -    o map (HOLogic.mk_number @{typ int} o @{code integer_of_int});
     1.9 +  val term_of_int_list = HOLogic.mk_list \<^typ>\<open>int\<close>
    1.10 +    o map (HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int});
    1.11  
    1.12 -  fun raw_sort (ctxt, ct, ks) = Thm.mk_binop @{cterm "Pure.eq :: int list \<Rightarrow> int list \<Rightarrow> prop"}
    1.13 +  fun raw_sort (ctxt, ct, ks) = Thm.mk_binop \<^cterm>\<open>Pure.eq :: int list \<Rightarrow> int list \<Rightarrow> prop\<close>
    1.14      ct (Thm.cterm_of ctxt (term_of_int_list ks));
    1.15  
    1.16    val (_, sort_oracle) = Context.>>> (Context.map_theory_result
    1.17 -    (Thm.add_oracle (@{binding sort}, raw_sort)));
    1.18 +    (Thm.add_oracle (\<^binding>\<open>sort\<close>, raw_sort)));
    1.19  
    1.20  in
    1.21  
    1.22 @@ -43,22 +43,22 @@
    1.23  
    1.24  declare [[code_timing]]
    1.25  
    1.26 -ML_val \<open>sort_int_abs_reversed_conv @{context}
    1.27 -  @{cterm "sort int_abs_reversed example_1"}\<close>
    1.28 +ML_val \<open>sort_int_abs_reversed_conv \<^context>
    1.29 +  \<^cterm>\<open>sort int_abs_reversed example_1\<close>\<close>
    1.30  
    1.31 -ML_val \<open>sort_int_abs_reversed_conv @{context}
    1.32 -  @{cterm "quicksort int_abs_reversed example_1"}\<close>
    1.33 +ML_val \<open>sort_int_abs_reversed_conv \<^context>
    1.34 +  \<^cterm>\<open>quicksort int_abs_reversed example_1\<close>\<close>
    1.35  
    1.36 -ML_val \<open>sort_int_abs_reversed_conv @{context}
    1.37 -  @{cterm "mergesort int_abs_reversed example_1"}\<close>
    1.38 +ML_val \<open>sort_int_abs_reversed_conv \<^context>
    1.39 +  \<^cterm>\<open>mergesort int_abs_reversed example_1\<close>\<close>
    1.40  
    1.41 -ML_val \<open>sort_int_abs_reversed_conv @{context}
    1.42 -  @{cterm "sort int_abs_reversed example_2"}\<close>
    1.43 +ML_val \<open>sort_int_abs_reversed_conv \<^context>
    1.44 +  \<^cterm>\<open>sort int_abs_reversed example_2\<close>\<close>
    1.45  
    1.46 -ML_val \<open>sort_int_abs_reversed_conv @{context}
    1.47 -  @{cterm "quicksort int_abs_reversed example_2"}\<close>
    1.48 +ML_val \<open>sort_int_abs_reversed_conv \<^context>
    1.49 +  \<^cterm>\<open>quicksort int_abs_reversed example_2\<close>\<close>
    1.50  
    1.51 -ML_val \<open>sort_int_abs_reversed_conv @{context}
    1.52 -  @{cterm "mergesort int_abs_reversed example_2"}\<close>
    1.53 +ML_val \<open>sort_int_abs_reversed_conv \<^context>
    1.54 +  \<^cterm>\<open>mergesort int_abs_reversed example_2\<close>\<close>
    1.55  
    1.56  end