src/HOL/Bali/WellType.thy
changeset 13462 56610e2ba220
parent 13384 a34e38154413
child 13524 604d0f3622d6
equal deleted inserted replaced
13461:f93f7d766895 13462:56610e2ba220
   618     | is_Inj _                   = false
   618     | is_Inj _                   = false
   619   fun pred (t as (_ $ (Const ("Pair",_) $
   619   fun pred (t as (_ $ (Const ("Pair",_) $
   620      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   620      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   621        x))) $ _ )) = is_Inj x
   621        x))) $ _ )) = is_Inj x
   622 in
   622 in
   623   make_simproc name lhs pred (thm name)
   623   cond_simproc name lhs pred (thm name)
   624 end
   624 end
   625 
   625 
   626 val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T"
   626 val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T"
   627 val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>=T"
   627 val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>=T"
   628 val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
   628 val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"