src/HOL/Nitpick.thy
changeset 60758 d8d85a8172b5
parent 58889 5b7a9633cfa8
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Nitpick.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  Nitpick: Yet another counterexample generator for Isabelle/HOL.
     1.5  *)
     1.6  
     1.7 -section {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
     1.8 +section \<open>Nitpick: Yet Another Counterexample Generator for Isabelle/HOL\<close>
     1.9  
    1.10  theory Nitpick
    1.11  imports Record
    1.12 @@ -30,9 +30,9 @@
    1.13    Quot :: "'a \<Rightarrow> 'b"
    1.14    safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.15  
    1.16 -text {*
    1.17 +text \<open>
    1.18  Alternative definitions.
    1.19 -*}
    1.20 +\<close>
    1.21  
    1.22  lemma Ex1_unfold[nitpick_unfold]: "Ex1 P \<equiv> \<exists>x. {x. P x} = {x}"
    1.23    apply (rule eq_reflection)
    1.24 @@ -79,10 +79,10 @@
    1.25    "fold_graph' f z {} z" |
    1.26    "\<lbrakk>x \<in> A; fold_graph' f z (A - {x}) y\<rbrakk> \<Longrightarrow> fold_graph' f z A (f x y)"
    1.27  
    1.28 -text {*
    1.29 +text \<open>
    1.30  The following lemmas are not strictly necessary but they help the
    1.31  \textit{specialize} optimization.
    1.32 -*}
    1.33 +\<close>
    1.34  
    1.35  lemma The_psimp[nitpick_psimp]: "P = (op =) x \<Longrightarrow> The P = x"
    1.36    by auto
    1.37 @@ -114,10 +114,10 @@
    1.38    "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
    1.39    by (cases xs) auto
    1.40  
    1.41 -text {*
    1.42 +text \<open>
    1.43  Auxiliary definitions used to provide an alternative representation for
    1.44  @{text rat} and @{text real}.
    1.45 -*}
    1.46 +\<close>
    1.47  
    1.48  function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    1.49    "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))"
    1.50 @@ -220,7 +220,7 @@
    1.51  ML_file "Tools/Nitpick/nitpick_commands.ML"
    1.52  ML_file "Tools/Nitpick/nitpick_tests.ML"
    1.53  
    1.54 -setup {*
    1.55 +setup \<open>
    1.56    Nitpick_HOL.register_ersatz_global
    1.57      [(@{const_name card}, @{const_name card'}),
    1.58       (@{const_name setsum}, @{const_name setsum'}),
    1.59 @@ -228,7 +228,7 @@
    1.60       (@{const_name wf}, @{const_name wf'}),
    1.61       (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
    1.62       (@{const_name wfrec}, @{const_name wfrec'})]
    1.63 -*}
    1.64 +\<close>
    1.65  
    1.66  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The FunBox PairBox Word prod
    1.67    refl' wf' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac