equal
deleted
inserted
replaced
655 the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}. |
655 the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}. |
656 *} |
656 *} |
657 |
657 |
658 local_setup %gray {* |
658 local_setup %gray {* |
659 Local_Theory.define ((@{binding "TrueConj"}, NoSyn), |
659 Local_Theory.define ((@{binding "TrueConj"}, NoSyn), |
660 (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *} |
660 ((@{binding "TrueConj_def"}, []), @{term "True \<and> True"})) #> snd *} |
661 |
661 |
662 text {* |
662 text {* |
663 Now querying the definition you obtain: |
663 Now querying the definition you obtain: |
664 |
664 |
665 \begin{isabelle} |
665 \begin{isabelle} |