before merge decompose-isar
authorJan Rocnik <jan.rocnik@student.tugraz.at>
Tue, 27 Sep 2011 11:05:00 +0200
branchdecompose-isar
changeset 42293b24574463e1a
parent 42292 5de15407e462
child 42294 9a25ba3bc281
before merge
doc-src/isac/jrocnik/Makefile
doc-src/isac/jrocnik/coursedirectory
doc-src/isac/jrocnik/fixbookmarks.pl
doc-src/isac/jrocnik/sedindex
src/Tools/isac/Knowledge/Partial_Fractions.thy
src/Tools/isac/Knowledge/Partial_Fractions.thy.bak
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/isac/jrocnik/Makefile	Tue Sep 27 11:05:00 2011 +0200
     1.3 @@ -0,0 +1,54 @@
     1.4 +## targets
     1.5 +
     1.6 +default: thesis clean
     1.7 +all: thesis docu clean
     1.8 +thesis: thesis clean
     1.9 +docu: docu clean
    1.10 +
    1.11 +
    1.12 +## dependencies
    1.13 +
    1.14 +
    1.15 +## settings
    1.16 +
    1.17 +LATEX = latex
    1.18 +PDFLATEX = pdflatex
    1.19 +BIBTEX = bibtex
    1.20 +RAIL = rail -a
    1.21 +SEDINDEX = ./sedindex
    1.22 +FIXBOOKMARKS = perl -pi fixbookmarks.pl
    1.23 +
    1.24 +DEFAULT_GARBAGE = *.aux *.log *.toc *.idx *.rai *.rao *.bbl *.ind *.ilg *.blg *.out *.lof
    1.25 +DEFAULT_OUTPUT = *.dvi *.pdf *.ps
    1.26 +GARBAGE =
    1.27 +OUTPUT =
    1.28 +
    1.29 +## special targets
    1.30 +
    1.31 +.DELETE_ON_ERROR:
    1.32 +
    1.33 +## actions
    1.34 +
    1.35 +nothing:
    1.36 +
    1.37 +clean:
    1.38 +	@rm -f $(DEFAULT_GARBAGE) $(GARBAGE)
    1.39 +
    1.40 +mrproper:
    1.41 +	@rm -f $(DEFAULT_GARBAGE) $(DEFAULT_OUTPUT) $(GARBAGE) $(OUTPUT)
    1.42 +
    1.43 +THESIS_NAME = bakkarbeit_jrocnik
    1.44 +THESIS_FILES = bakkarbeit_jrocnik.tex
    1.45 +
    1.46 +DOCU_NAME = Inverse_Z_Transform/doc/Inverse_Z_Transform
    1.47 +DOCU_FILES = Inverse_Z_Transform/doc/root.tex 
    1.48 +
    1.49 +thesis: $(THESIS_NAME).pdf
    1.50 +
    1.51 +$(THESIS_NAME).pdf: $(THESIS_FILES)
    1.52 +	$(PDFLATEX) $(THESIS_NAME)
    1.53 +	$(BIBTEX) $(THESIS_NAME)
    1.54 +	$(PDFLATEX) $(THESIS_NAME)
    1.55 +	$(PDFLATEX) $(THESIS_NAME)
    1.56 +  
    1.57 +docu:
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/isac/jrocnik/coursedirectory	Tue Sep 27 11:05:00 2011 +0200
     2.3 @@ -0,0 +1,1 @@
     2.4 +../../../test/Tools/isac/ADDTESTS/course/SignalProcess
     2.5 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/isac/jrocnik/fixbookmarks.pl	Tue Sep 27 11:05:00 2011 +0200
     3.3 @@ -0,0 +1,4 @@
     3.4 +
     3.5 +s/\\([a-zA-Z]+)\s*/$1/g;
     3.6 +s/\$//g;
     3.7 +s/^BOOKMARK/\\BOOKMARK/g;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/isac/jrocnik/sedindex	Tue Sep 27 11:05:00 2011 +0200
     4.3 @@ -0,0 +1,21 @@
     4.4 +#! /bin/sh
     4.5 +#
     4.6 +#sedindex - shell script to create indexes, preprocessing LaTeX's .idx file
     4.7 +#
     4.8 +#  puts strings prefixed by * into \tt font
     4.9 +#    terminator characters for strings are |!@{}
    4.10 +#
    4.11 +# a space terminates the \tt part to allow \index{*NE theorem}, etc.
    4.12 +#
    4.13 +# change *"X"Y"Z"W  to  "X"Y"Z"W@{\tt "X"Y"Z"W}
    4.14 +# change *"X"Y"Z    to  "X"Y"Z@{\tt "X"Y"Z}
    4.15 +# change *"X"Y      to  "X"Y@{\tt "X"Y}
    4.16 +# change *"X        to  "X@{\tt "X}
    4.17 +# change *IDENT  to  IDENT@{\tt IDENT}  
    4.18 +#    where IDENT is any string not containing | ! or @
    4.19 +# FOUR backslashes: to escape the shell AND sed
    4.20 +sed -e "s~\*\(\".\".\".\".\)~\1@{\\\\tt \1}~g
    4.21 +s~\*\(\".\".\".\)~\1@{\\\\tt \1}~g
    4.22 +s~\*\(\".\".\)~\1@{\\\\tt \1}~g
    4.23 +s~\*\(\".\)~\1@{\\\\tt \1}~g
    4.24 +s~\*\([^ |!@{}][^ |!@{}]*\)~\1@{\\\\tt \1}~g" $1.idx | makeindex -c -q -o $1.ind
     5.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Tue Sep 27 11:00:49 2011 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Tue Sep 27 11:05:00 2011 +0200
     5.3 @@ -11,22 +11,42 @@
     5.4  	          Trueprop $ (mk_equality (t, denom)))
     5.5    | eval_get_denominator _ _ _ _ = NONE; 
     5.6  *}
     5.7 -text {*rule set for partial fractions*}
     5.8 +
     5.9 +
    5.10 +
    5.11 +subsection {*get the argument out of a fraction*}
    5.12 +
    5.13 +ML {*
    5.14 +(*("get_argument", ("Rational.get'_argument", eval_get_argument ""))*)
    5.15 +
    5.16 +(* 
    5.17 +fun eval_get_argument "Atools.argument'_in" 
    5.18 +		     (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
    5.19 +    if is_Free arg (*could be something to be simplified before*)
    5.20 +    then SOME (term2str t ^ " = " ^ term2str arg,
    5.21 +	       Trueprop $ (mk_equality (t, arg)))
    5.22 +    else NONE
    5.23 +  | eval_argument_in _ _ _ _ = NONE;
    5.24 +*)
    5.25 +
    5.26 +*}
    5.27 +
    5.28 +subsection{*rule set for partial fractions*}
    5.29  ML {*
    5.30  val partial_fraction = 
    5.31    Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), 
    5.32  	  erls = Erls, srls = Erls, calc = [],
    5.33  	  rules = [
    5.34 -				    Calc ("Rings.inverse_class.divide", eval_get_denominator "#")
    5.35 +				    Calc ("Rings.inverse_class.divide", eval_get_denominator "#", eval_get_argument "X")
    5.36  		  ],
    5.37  	 scr = EmptyScr};
    5.38  *}
    5.39 -text {*store the rule set for math engine*}
    5.40 +
    5.41 +subsection{*store the rule set for math engine*}
    5.42  ML {*
    5.43    overwritelthy @{theory} (!ruleset', 
    5.44  	    [("partial_fraction", prep_rls partial_fraction)
    5.45  	     ]);
    5.46  *}
    5.47  
    5.48 -
    5.49  end
    5.50 \ No newline at end of file
     6.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy.bak	Tue Sep 27 11:00:49 2011 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,65 +0,0 @@
     6.4 -theory Partial_Fractions imports Rational begin
     6.5 -
     6.6 -subsection {*get the denominator out of a fraction*}
     6.7 -text {*this function can be put into rule sets*}
     6.8 -ML {*
     6.9 -(*("get_denominator", ("Rational.get'_denominator", eval_get_denominator ""))*)
    6.10 -fun eval_get_denominator (thmid:string) _ 
    6.11 -		      (t as (Const("Rings.inverse_class.divide", _) $ num $ denom)) thy = 
    6.12 -    SOME (mk_thmid thmid "" 
    6.13 -            (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) denom) "", 
    6.14 -	          Trueprop $ (mk_equality (t, denom)))
    6.15 -  | eval_get_denominator _ _ _ _ = NONE; 
    6.16 -
    6.17 -
    6.18 -
    6.19 -*}
    6.20 -
    6.21 -
    6.22 -
    6.23 -subsection {*get the argument out of a fraction*}
    6.24 -
    6.25 -ML {*(*
    6.26 -(*("get_argument", ("Rational.get'_argument", eval_get_argument ""))*)
    6.27 -
    6.28 -
    6.29 -fun eval_get_argument "Atools.argument'_in" 
    6.30 -		     (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
    6.31 -    if is_Free arg (*could be something to be simplified before*)
    6.32 -    then SOME (term2str t ^ " = " ^ term2str arg,
    6.33 -	       Trueprop $ (mk_equality (t, arg)))
    6.34 -    else NONE
    6.35 -  | eval_get_argument_in _ _ _ _ = NONE;
    6.36 -*)
    6.37 -*}
    6.38 -
    6.39 -
    6.40 -subsection {*store the function for fetching from script*}
    6.41 -
    6.42 -ML {*
    6.43 -calclist' := overwritel (!calclist',
    6.44 -  [
    6.45 -    ("get_denominator", ("Rational.get'_denominator", eval_get_denominator "")),
    6.46 -    ("get_argument", ("Rational.get'_argument", eval_get_argument ""))
    6.47 -  ]);
    6.48 -*}
    6.49 -
    6.50 -subsection{*rule set for partial fractions*}
    6.51 -ML {*
    6.52 -val partial_fraction = 
    6.53 -  Rls {id="partial_fraction", preconds = [], rew_ord = ("termlessI",termlessI), 
    6.54 -	  erls = Erls, srls = Erls, calc = [],
    6.55 -	  rules = [
    6.56 -				    Calc ("Rings.inverse_class.divide", eval_get_denominator "#", eval_get_argument "X")
    6.57 -		  ],
    6.58 -	 scr = EmptyScr};
    6.59 -*}
    6.60 -
    6.61 -subsection{*store the rule set for math engine*}
    6.62 -ML {*
    6.63 -  overwritelthy @{theory} (!ruleset', 
    6.64 -	    [("partial_fraction", prep_rls partial_fraction)
    6.65 -	     ]);
    6.66 -*}
    6.67 -
    6.68 -end
    6.69 \ No newline at end of file