src/HOL/Predicate_Compile.thy
changeset 60758 d8d85a8172b5
parent 58889 5b7a9633cfa8
child 62390 842917225d56
     1.1 --- a/src/HOL/Predicate_Compile.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Predicate_Compile.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* A compiler for predicates defined by introduction rules *}
     1.8 +section \<open>A compiler for predicates defined by introduction rules\<close>
     1.9  
    1.10  theory Predicate_Compile
    1.11  imports Random_Sequence Quickcheck_Exhaustive
    1.12 @@ -22,12 +22,12 @@
    1.13  ML_file "Tools/Predicate_Compile/predicate_compile.ML"
    1.14  
    1.15  
    1.16 -subsection {* Set membership as a generator predicate *}
    1.17 +subsection \<open>Set membership as a generator predicate\<close>
    1.18  
    1.19 -text {* 
    1.20 +text \<open>
    1.21    Introduce a new constant for membership to allow 
    1.22    fine-grained control in code equations. 
    1.23 -*}
    1.24 +\<close>
    1.25  
    1.26  definition contains :: "'a set => 'a => bool"
    1.27  where "contains A x \<longleftrightarrow> x : A"
    1.28 @@ -68,7 +68,7 @@
    1.29     "\<not> contains A x ==> Predicate.eval (Predicate.not_pred (contains_pred A x)) ()"
    1.30  by(simp add: contains_pred_def contains_def not_pred_eq)
    1.31  
    1.32 -setup {*
    1.33 +setup \<open>
    1.34  let
    1.35    val Fun = Predicate_Compile_Aux.Fun
    1.36    val Input = Predicate_Compile_Aux.Input
    1.37 @@ -97,7 +97,7 @@
    1.38            })],
    1.39         needs_random = []}))
    1.40  end
    1.41 -*}
    1.42 +\<close>
    1.43  
    1.44  hide_const (open) contains contains_pred
    1.45  hide_fact (open) pred_of_setE pred_of_setI pred_of_set_eq