src/Tools/isac/Knowledge/DiffApp.thy
branchdecompose-isar
changeset 41905 b772eb34c16c
parent 38045 ac0f6fd8d129
child 42197 7497ff20f1e8
     1.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Sat Feb 26 12:53:00 2011 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Tue Mar 01 15:23:59 2011 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4  (*primrec*)axioms
     1.5    filterVar_Nil:		"filterVar v []     = []"
     1.6    filterVar_Const:	"filterVar v (x#xs) =                       
     1.7 -			 (if (v mem (Vars x)) then x#(filterVar v xs)  
     1.8 +			 (if (v : set (Vars x)) then x#(filterVar v xs)  
     1.9  			                    else filterVar v xs)   "
    1.10  text {*WN.6.5.03: old decisions in this file partially are being changed
    1.11    in a quick-and-dirty way to make scripts run: Maximum_value,