equal
deleted
inserted
replaced
656 *} |
656 *} |
657 |
657 |
658 ML {* |
658 ML {* |
659 @{context} |
659 @{context} |
660 |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) |
660 |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) |
661 ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"}) |
|
662 ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"}) |
|
663 *} |
|
664 |
|
665 ML {* |
|
666 val ((((One, One_thm), (Two, Two_thm)), (Three, Three_thm)), _)) = |
|
667 @{context} |
|
668 |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) |
|
669 ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"}) |
661 ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"}) |
670 ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"}) |
662 ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"}) |
671 *} |
663 *} |
672 |
664 |
673 |
665 |