equal
deleted
inserted
replaced
878 lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A" |
878 lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A" |
879 by (auto simp add: the_def singleton_def not_unique_def) |
879 by (auto simp add: the_def singleton_def not_unique_def) |
880 |
880 |
881 code_abort not_unique |
881 code_abort not_unique |
882 |
882 |
883 code_reflect |
883 code_reflect Predicate |
884 datatypes pred = Seq and seq = Empty | Insert | Join |
884 datatypes pred = Seq and seq = Empty | Insert | Join |
885 functions map |
885 functions map |
886 module_name Predicate |
|
887 |
886 |
888 ML {* |
887 ML {* |
889 signature PREDICATE = |
888 signature PREDICATE = |
890 sig |
889 sig |
891 datatype 'a pred = Seq of (unit -> 'a seq) |
890 datatype 'a pred = Seq of (unit -> 'a seq) |