src/HOL/Bali/Basis.thy
changeset 13688 a0b16d42d489
parent 13462 56610e2ba220
child 13867 1fdecd15437f
     1.1 --- a/src/HOL/Bali/Basis.thy	Wed Oct 30 12:44:18 2002 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Thu Oct 31 18:27:10 2002 +0100
     1.3 @@ -247,6 +247,12 @@
     1.4  	"In1l e" == "In1 (Inl e)"
     1.5  	"In1r c" == "In1 (Inr c)"
     1.6  
     1.7 +syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
     1.8 +       the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
     1.9 +translations
    1.10 +   "the_In1l" == "the_Inl \<circ> the_In1"
    1.11 +   "the_In1r" == "the_Inr \<circ> the_In1"
    1.12 +
    1.13  ML {*
    1.14  fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[not_None_eq])
    1.15   (read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"]