src/HOL/Bali/DefiniteAssignmentCorrect.thy
changeset 35069 09154b995ed8
parent 32960 69916a850301
child 44890 22f665a2e91c
equal deleted inserted replaced
35068:544867142ea4 35069:09154b995ed8
     1 (* $Id$ *)
       
     2 
       
     3 header {* Correctness of Definite Assignment *}
     1 header {* Correctness of Definite Assignment *}
     4 
     2 
     5 theory DefiniteAssignmentCorrect imports WellForm Eval begin
     3 theory DefiniteAssignmentCorrect imports WellForm Eval begin
     6 
     4 
     7 declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
     5 declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]