equal
deleted
inserted
replaced
638 |
638 |
639 hide (open) type pred seq |
639 hide (open) type pred seq |
640 hide (open) const Pred eval single bind if_pred not_pred |
640 hide (open) const Pred eval single bind if_pred not_pred |
641 Empty Insert Join Seq member pred_of_seq "apply" adjunct eq |
641 Empty Insert Join Seq member pred_of_seq "apply" adjunct eq |
642 |
642 |
|
643 text {* dummy setup for code_pred keyword *} |
|
644 |
|
645 ML {* |
|
646 OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate" |
|
647 OuterKeyword.thy_goal (OuterParse.term_group >> (K (Proof.theorem_i NONE (K I) [[]]))) |
|
648 *} |
|
649 |
|
650 |
643 end |
651 end |