src/HOL/Library/Simps_Case_Conv.thy
changeset 53426 92db671e0ac6
child 53433 3b356b7f7cad
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Simps_Case_Conv.thy	Fri Sep 06 10:56:40 2013 +0200
     1.3 @@ -0,0 +1,12 @@
     1.4 +(*  Title:    HOL/Library/Simps_Case_Conv.thy
     1.5 +    Author:   Lars Noschinski
     1.6 +*)
     1.7 +
     1.8 +theory Simps_Case_Conv
     1.9 +  imports Main
    1.10 +  keywords "simps_of_case" "case_of_simps" :: thy_decl
    1.11 +begin
    1.12 +
    1.13 +ML_file "simps_case_conv.ML"
    1.14 +
    1.15 +end