src/FOL/IFOL.thy
changeset 4092 9faf228771dc
parent 3932 436463f9f2b4
child 4793 03fd006fb97b
equal deleted inserted replaced
4091:771b1f6422a8 4092:9faf228771dc
   110 
   110 
   111   eq_reflection   "(x=y)   ==> (x==y)"
   111   eq_reflection   "(x=y)   ==> (x==y)"
   112   iff_reflection  "(P<->Q) ==> (P==Q)"
   112   iff_reflection  "(P<->Q) ==> (P==Q)"
   113 
   113 
   114 end
   114 end
       
   115 
       
   116 
       
   117 ML val thy_data = [Simplifier.simpset_thy_data];