1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/java/CalcHeadPanel.properties	Thu May 10 11:06:34 2007 +0200
     1.3 @@ -0,0 +1,10 @@
     1.4 +fullCH=full CalcHead
     1.5 +given=Given
     1.6 +where=Where
     1.7 +find=Find
     1.8 +theory=Theory
     1.9 +method=Method
    1.10 +problem=Problem
    1.11 +relate=Relate
    1.12 +submit=Submit
    1.13 +solve=Solve
    1.14 \ No newline at end of file

     2.1 --- a/src/sml/IsacKnowledge/Atools.ML	Thu May 03 10:33:00 2007 +0200
     2.2 +++ b/src/sml/IsacKnowledge/Atools.ML	Thu May 10 11:06:34 2007 +0200
     2.3 @@ -388,6 +388,25 @@
     2.4  | eval_sameFunId _ _ _ _ = None;
     2.5  
     2.6  
     2.7 +(*.from a list of fun-definitions "f x = ..." as 2nd argument
     2.8 +   filter the elements with the same fun-identfier in "f y"
     2.9 +   as the fst argument;
    2.10 +   this is, because Isabelles filter takes more than 1 sec.*)
    2.11 +fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2
    2.12 +  | same_funid f1 t = raise error ("same_funid called with t = ("
    2.13 +				   ^term2str f1^") ("^term2str t^")");
    2.14 +(*("filter_sameFunId" ,("Atools.filter'_sameFunId",
    2.15 +		   eval_filter_sameFunId "Atools.filter'_sameFunId"))*)
    2.16 +fun eval_filter_sameFunId _ "Atools.filter'_sameFunId" 
    2.17 +		     (p as Const ("Atools.filter'_sameFunId",_) $ 
    2.18 +			(fid $ _) $ fs) _ =
    2.19 +    let val fs' = ((list2isalist HOLogic.boolT) o 
    2.20 +		   (filter (same_funid fid))) (isalist2list fs)
    2.21 +    in Some (term2str (mk_equality (p, fs')),
    2.22 +	       Trueprop $ (mk_equality (p, fs'))) end
    2.23 +| eval_filter_sameFunId _ _ _ _ = None;
    2.24 +
    2.25 +
    2.26  (*make a list of terms to a sum*)
    2.27  fun list2sum [] = error ("list2sum called with []")
    2.28    | list2sum [s] = s