1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Wed Feb 07 10:24:16 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Wed Feb 07 11:21:54 2018 +0100
1.3 @@ -1,4 +1,4 @@
1.4 -header {* GCD for polynomials by the function package following GCD_Poly_ML *}
1.5 +(* GCD for polynomials by the function package following GCD_Poly_ML *)
1.6 theory GCD_Poly_FP
1.7 imports "~~/src/HOL/Computational_Algebra/Polynomial"
1.8 "~~/src/HOL/Computational_Algebra/Primes"
2.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_OLD.thy Wed Feb 07 10:24:16 2018 +0100
2.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_OLD.thy Wed Feb 07 11:21:54 2018 +0100
2.3 @@ -1,5 +1,5 @@
2.4 -header {* 1st approach to Isabelle's new Polynomials;
2.5 - continued in TPPL/material/AD_Polynomal.thy*}
2.6 +(* 1st approach to Isabelle's new Polynomials
2.7 + continued in TPPL/material/AD_Polynomal.thy *)
2.8
2.9 theory GCD_Poly_OLD
2.10 imports "~~/src/HOL/Computational_Algebra/Polynomial"
3.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Wed Feb 07 10:24:16 2018 +0100
3.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Wed Feb 07 11:21:54 2018 +0100
3.3 @@ -1,4 +1,4 @@
3.4 -(* this is evaluated BEFORE Test_Isac.thu opens structures*)
3.5 +(* this is evaluated BEFORE Test_Isac.thy opens structures*)
3.6
3.7 theory All_Ctxt imports
3.8 "~~/src/Tools/isac/Knowledge/Isac"
4.1 --- a/test/Tools/isac/ADDTESTS/Hints.thy Wed Feb 07 10:24:16 2018 +0100
4.2 +++ b/test/Tools/isac/ADDTESTS/Hints.thy Wed Feb 07 11:21:54 2018 +0100
4.3 @@ -1,4 +1,4 @@
4.4 -header {* hints on Isabelle system usage *}
4.5 +(* hints on Isabelle system usage *)
4.6
4.7 theory Hints imports Main begin
4.8
5.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML1_Basics.thy Wed Feb 07 10:24:16 2018 +0100
5.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML1_Basics.thy Wed Feb 07 11:21:54 2018 +0100
5.3 @@ -1,4 +1,4 @@
5.4 -header {* Quick introduction to ML, session 1 *}
5.5 +(* Quick introduction to ML, session 1 *)
5.6 theory ML1_Basics imports Isac begin
5.7
5.8 text{* This course follows the book:
6.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML2_Functions.thy Wed Feb 07 10:24:16 2018 +0100
6.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML2_Functions.thy Wed Feb 07 11:21:54 2018 +0100
6.3 @@ -1,4 +1,4 @@
6.4 -header {* Quick introduction to ML, session 2 *}
6.5 +(* Quick introduction to ML, session 2 *)
6.6 theory ML2_Functions imports Isac begin
6.7
6.8 text{*
7.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML3_Combinators.thy Wed Feb 07 10:24:16 2018 +0100
7.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML3_Combinators.thy Wed Feb 07 11:21:54 2018 +0100
7.3 @@ -1,4 +1,4 @@
7.4 -header {* Quick introduction to ML, session 3 *}
7.5 +(* Quick introduction to ML, session 3 *)
7.6
7.7 theory ML3_Combinators imports Isac begin
7.8
8.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML4_Datastructure.thy Wed Feb 07 10:24:16 2018 +0100
8.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML4_Datastructure.thy Wed Feb 07 11:21:54 2018 +0100
8.3 @@ -1,4 +1,4 @@
8.4 -header {* Quick introduction to ML, session 3 *}
8.5 +(* Quick introduction to ML, session 3 *)
8.6
8.7 theory ML4_Datastructure imports Isac begin
8.8
9.1 --- a/test/Tools/isac/ADDTESTS/test-depend/Build_Test.thy Wed Feb 07 10:24:16 2018 +0100
9.2 +++ b/test/Tools/isac/ADDTESTS/test-depend/Build_Test.thy Wed Feb 07 11:21:54 2018 +0100
9.3 @@ -1,10 +1,8 @@
9.4 -(* Title: test/../test-depend/Build_Test.thy
9.5 +(* Title: file dependencies according to Test_Isac.thy
9.6 Author: Walther Neuper 110320
9.7 (c) copyright due to lincense terms.
9.8 *)
9.9
9.10 -header {* file dependencies according to Test_Isac.thy *}
9.11 -
9.12 theory Build_Test
9.13 imports Main "testdir1/testdir1" "testdirm/testdirm"
9.14 begin
10.1 --- a/test/Tools/isac/ADDTESTS/test-depend/testdir1/testdir1.thy Wed Feb 07 10:24:16 2018 +0100
10.2 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdir1/testdir1.thy Wed Feb 07 11:21:54 2018 +0100
10.3 @@ -1,10 +1,8 @@
10.4 -(* Title: test/../test-depend/testdir1.thy
10.5 +(* Title: collect all testfiles in directory testdir1/
10.6 Author: Walther Neuper 110320
10.7 (c) copyright due to lincense terms.
10.8 *)
10.9
10.10 -header {* collect all testfiles in directory testdir1/ *}
10.11 -
10.12 theory testdir1
10.13 imports Main
10.14 begin
11.1 --- a/test/Tools/isac/ADDTESTS/test-depend/testdirm/testdirm.thy Wed Feb 07 10:24:16 2018 +0100
11.2 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdirm/testdirm.thy Wed Feb 07 11:21:54 2018 +0100
11.3 @@ -1,10 +1,8 @@
11.4 -(* Title: test/../test-depend/testdirm/testdirm.thy
11.5 +(* Title: collect all testfiles in directory testdirm/
11.6 Author: Walther Neuper 110320
11.7 (c) copyright due to lincense terms.
11.8 *)
11.9
11.10 -header {* collect all testfiles in directory testdirm/ *}
11.11 -
11.12 theory testdirm
11.13 imports Main
11.14 begin
12.1 --- a/test/Tools/isac/CLEANUP Wed Feb 07 10:24:16 2018 +0100
12.2 +++ b/test/Tools/isac/CLEANUP Wed Feb 07 11:21:54 2018 +0100
12.3 @@ -64,6 +64,20 @@
12.4 rm .\#*
12.5 rm *.tar*
12.6 rm *.orig*
12.7 + cd testdir1
12.8 + rm *~
12.9 + rm #*
12.10 + rm .\#*
12.11 + rm *.tar*
12.12 + rm *.orig*
12.13 + cd ..
12.14 + cd testdirm
12.15 + rm *~
12.16 + rm #*
12.17 + rm .\#*
12.18 + rm *.tar*
12.19 + rm *.orig*
12.20 + cd ..
12.21 cd ..
12.22 cd ..
12.23 cd ProgLang