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