equal
deleted
inserted
replaced
829 [code del]: "the A = (THE x. eval A x)" |
829 [code del]: "the A = (THE x. eval A x)" |
830 |
830 |
831 lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A" |
831 lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A" |
832 by (auto simp add: the_def singleton_def not_unique_def) |
832 by (auto simp add: the_def singleton_def not_unique_def) |
833 |
833 |
|
834 code_abort not_unique |
|
835 |
834 ML {* |
836 ML {* |
835 signature PREDICATE = |
837 signature PREDICATE = |
836 sig |
838 sig |
837 datatype 'a pred = Seq of (unit -> 'a seq) |
839 datatype 'a pred = Seq of (unit -> 'a seq) |
838 and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq |
840 and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq |
874 (Eval "_/ Predicate.pred" and "_/ Predicate.seq") |
876 (Eval "_/ Predicate.pred" and "_/ Predicate.seq") |
875 |
877 |
876 code_const Seq and Empty and Insert and Join |
878 code_const Seq and Empty and Insert and Join |
877 (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)") |
879 (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)") |
878 |
880 |
879 code_abort not_unique |
|
880 |
|
881 no_notation |
881 no_notation |
882 inf (infixl "\<sqinter>" 70) and |
882 inf (infixl "\<sqinter>" 70) and |
883 sup (infixl "\<squnion>" 65) and |
883 sup (infixl "\<squnion>" 65) and |
884 Inf ("\<Sqinter>_" [900] 900) and |
884 Inf ("\<Sqinter>_" [900] 900) and |
885 Sup ("\<Squnion>_" [900] 900) and |
885 Sup ("\<Squnion>_" [900] 900) and |