src/HOL/Library/Simps_Case_Conv.thy
author wenzelm
Mon Jul 11 09:57:20 2016 +0200 (2016-07-11)
changeset 63432 ba7901e94e7b
parent 56361 9f9f60f4dbbf
child 63579 73939a9b70a3
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Library/Simps_Case_Conv.thy
     2     Author:     Lars Noschinski
     3 *)
     4 
     5 theory Simps_Case_Conv
     6 imports Main
     7 keywords
     8   "simps_of_case" :: thy_decl == "" and
     9   "case_of_simps" :: thy_decl
    10 begin
    11 
    12 ML_file "simps_case_conv.ML"
    13 
    14 end