1 (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
2 Author: Walther Neuper 101001
3 (c) copyright due to lincense terms.
5 Isac's tests are organised parallel to sources:
6 "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
8 ~~/test/Tools/isac/ADDTESTS
9 ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
11 $ cd /usr/local/isabisac/
12 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
15 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
16 (* !!!!! say "OK" to the popup asking for theories to be loaded and !!!!!!!!!!!!! *)
17 (* !!!!! watch the <Theories> window for errors in the "imports" below !!!!!!!!!! *)
18 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
20 theory Test_Isac imports Build_Thydata
21 "ADDTESTS/accumulate-val/Thy_All"
23 "ADDTESTS/test-depend/Build_Test"
25 "ADDTESTS/course/phst11/T1_Basics"
26 "ADDTESTS/course/phst11/T2_Rewriting"
27 "ADDTESTS/course/phst11/T3_MathEngine"
28 "ADDTESTS/file-depend/BuildC_Test"
29 "ADDTESTS/session-get_theory/Foo"
30 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
31 ADDTESTS/------------------------------------------- see end of tests *)
32 (*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *)
33 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
34 "~~/test/Pure/Isar/Test_Parse_Term"
35 "~~/test/HOL/Library/Test_Polynomial"
36 "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
37 "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*)
38 "~~/test/Tools/isac/ProgLang/scrtools" (* setup for scrtools.sml *)
39 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
41 "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
42 "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
47 KEStore_Elems.set_ref_thy @{theory};
48 fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*);
51 section {* trials with Isabelle's functions *}
52 ML {*"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";*}
53 ML_file "~~/test/Pure/General/alist.ML"
54 ML_file "~~/test/Pure/General/basics.ML"
55 ML_file "~~/test/Pure/General/scan.ML"
56 ML_file "~~/test/Pure/PIDE/xml.ML"
57 ML {*"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";*}
59 section {* test ML Code of isac *}
60 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
62 ML_file "calcelems.sml"
64 ML_file "ProgLang/termC.sml"
65 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
66 ML_file "ProgLang/rewrite.sml"
67 ML_file "ProgLang/listC.sml"
68 ML_file "ProgLang/scrtools.sml"
69 ML_file "ProgLang/tools.sml"
70 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
71 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
72 ML_file "Minisubpbl/000-comments.sml"
73 ML_file "Minisubpbl/100-init-rootpbl.sml"
74 ML_file "Minisubpbl/150-add-given.sml"
75 ML_file "Minisubpbl/200-start-method.sml"
76 ML_file "Minisubpbl/300-init-subpbl.sml"
77 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
78 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
79 ML_file "Minisubpbl/500-met-sub-to-root.sml"
80 ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
81 ML_file "Minisubpbl/600-postcond.sml"
82 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
83 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
84 ML_file "Interpret/mstools.sml"
85 ML_file "Interpret/ctree.sml" (*!...!see(25)*)
86 ML_file "Interpret/ptyps.sml" (* requires setup from ptyps.thy *)
87 ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
88 (*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)
89 ML_file "Interpret/generate.sml"
90 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
91 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
92 ML_file "Interpret/calchead.sml"
93 ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
94 ML_file "Interpret/rewtools.sml"
95 ML_file "Interpret/script.sml"
96 ML_file "Interpret/solve.sml"
97 ML_file "Interpret/inform.sml"
98 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
99 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
100 ML_file "Interpret/mathengine.sml" (*!part. WN130804: +check Interpret/me.sml*)
101 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
102 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
103 ML_file "xmlsrc/mathml.sml" (*part.*)
104 ML_file "xmlsrc/datatypes.sml" (*TODO/part.*)
105 ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
106 ML_file "xmlsrc/thy-hierarchy.sml"
107 ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
108 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
109 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
110 ML_file "Frontend/messages.sml"
111 ML_file "Frontend/states.sml"
112 ML_file "Frontend/interface.sml"
113 ML_file "Frontend/use-cases.sml"
114 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
115 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
116 ML_file "print_exn_G.sml"
117 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
118 ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*}
119 ML_file "Knowledge/delete.sml"
120 ML_file "Knowledge/descript.sml"
121 ML_file "Knowledge/atools.sml"
122 ML_file "Knowledge/simplify.sml"
123 ML_file "Knowledge/poly.sml"
124 ML_file "Knowledge/gcd_poly_ml.sml"
125 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
126 ML_file "Knowledge/rational.sml"
127 ML_file "Knowledge/equation.sml"
128 ML_file "Knowledge/root.sml"
129 ML_file "Knowledge/lineq.sml"
130 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
131 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
132 ML_file "Knowledge/rootrat.sml"
133 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
134 ML_file "Knowledge/partial_fractions.sml"
135 ML_file "Knowledge/polyeq.sml"
136 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
137 ML_file "Knowledge/calculus.sml"
138 ML_file "Knowledge/trig.sml"
139 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
140 ML_file "Knowledge/diff.sml"
141 ML_file "Knowledge/integrate.sml"
142 ML_file "Knowledge/eqsystem.sml"
143 ML_file "Knowledge/test.sml"
144 ML_file "Knowledge/polyminus.sml"
145 ML_file "Knowledge/vect.sml"
146 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
147 ML_file "Knowledge/biegelinie.sml"
148 ML_file "Knowledge/algein.sml"
149 ML_file "Knowledge/diophanteq.sml"
150 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
151 ML_file "Knowledge/isac.sml"
152 ML_file "Knowledge/build_thydata.sml"
153 ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
154 ML {*"%%%%%%%%%%%%%%%%% start ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%";*}
155 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
156 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
157 ML {*"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";*}
159 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
160 ML {*"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";*}
161 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
163 section {* history of tests *}
165 Systematic regression tests have been introduced to isac development in 2003.
166 Sanity of the regression tests suffers from updates following Isabelle development,
167 which mostly exceeded the resources available in isac's development.
169 The survey below shall support to efficiently use the tests for isac
170 on different Isabelle versions. Conclusion in most cases will be:
172 !!! Use most recent tests or go back to the old notebook
173 with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
176 subsection {* isac on Isabelle2014 *}
177 subsubsection {* Summary of development *}
179 migration from "isabelle tty" --> libisabelle
182 subsection {* isac on Isabelle2013-2 *}
183 subsubsection {* Summary of development *}
185 reactivated context_thy
187 subsubsection {* State of tests *}
191 subsubsection {* Changesets of begin and end *}
195 : isac on Isablle2013-2
197 Changeset: 55318 (03826ceb24da) merged
198 User: Walther Neuper <neuper@ist.tugraz.at>
199 Date: 2013-12-12 14:27:37 +0100 (7 minutes)
202 subsection {* isac on Isabelle2013-1 *}
203 subsubsection {* Summary of development *}
205 Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
206 no significant development steps for ISAC.
208 subsubsection {* State of tests *}
210 See points in subsection "isac on Isabelle2011", "State of tests".
212 subsubsection {* Changesets of begin and end *}
214 Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
215 User: Walther Neuper <neuper@ist.tugraz.at>
216 Date: 2013-12-03 18:13:31 +0100 (8 days)
218 : isac on Isablle2013-1
220 Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
221 User: Walther Neuper <neuper@ist.tugraz.at>
222 Date: 2013-11-21 18:12:17 +0100 (2 weeks)
226 subsection {* isac on Isabelle2013 *}
227 subsubsection {* Summary of development *}
229 # Oct.13: replaced "axioms" by "axiomatization"
230 # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
231 # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
232 simplification of multivariate rationals (without improving the rulesets involved).
234 subsubsection {* Run tests *}
236 Is standard now; this subsection will be discontinued under Isabelle2013-1
238 subsubsection {* State of tests *}
240 See points in subsection "isac on Isabelle2011", "State of tests".
241 # re-activated listC.sml
243 subsubsection {* Changesets of begin and end *}
245 changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
246 User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
247 Date: Tue Nov 19 22:23:30 2013 +0000
249 : isac on Isablle2013
251 Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
252 User: Walther Neuper <neuper@ist.tugraz.at>
253 Date: 2013-07-15 08:28:50 +0200 (4 weeks)
256 subsection {* isac on Isabelle2012 *}
257 subsubsection {* Summary of development *}
259 isac on Isabelle2012 is considered just a transitional stage
260 within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
261 For considerations on the transition see
262 ~~/src/Tools/isac/Knowledge/Build_Thydata/thy, section "updating isac..".
264 subsubsection {* Run tests *}
266 $ cd /usr/local/isabisac12/
267 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
268 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
270 subsubsection {* State of tests *}
272 At least the tests from isac on Isabelle2011 run again.
273 However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
274 in parallel with evaluation.
276 Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
277 yields 69 hits, some of which were already present before Isabelle2002-->2009-2
278 (i.e. on the old notebook from 2002).
280 Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin:
281 # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
282 # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
283 # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
284 Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
286 Some tests have been re-activated (e.g. error patterns, fill patterns).
288 subsubsection {* Changesets of begin and end *}
290 Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
291 User: Walther Neuper <neuper@ist.tugraz.at>
292 Date: 2013-07-11 16:58:31 +0200 (4 weeks)
294 : isac on Isablle2012
296 Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
297 User: Walther Neuper <neuper@ist.tugraz.at>
298 Date: 2012-09-24 18:35:13 +0200 (8 months)
299 ------------------------------------------------------------------------------
300 Changeset: 48756 (7443906996a8) merged
301 User: Walther Neuper <neuper@ist.tugraz.at>
302 Date: 2012-09-24 18:15:49 +0200 (8 months)
305 subsection {* isac on Isabelle2011 *}
306 subsubsection {* Summary of development *}
308 isac's mathematics engine has been extended by two developments:
309 (1) Isabelle's contexts were introduced by Mathias Lehnfeld
310 (2) Z_Transform was introduced by Jan Rocnik, which revealed
311 further errors introduced by (1).
312 (3) "error patterns" were introduced by Gabriella Daroczy
313 Regressions tests have been added for all of these.
315 subsubsection {* Run tests *}
317 $ cd /usr/local/isabisac11/
318 $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
319 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
321 subsubsection {* State of tests *}
323 Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*)
324 and sometimes give reasons for failing tests.
325 (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable
326 work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
328 The most signification tests (in particular Frontend/interface.sml) run,
329 however, many "error in kernel" are not caught by an exception.
330 ------------------------------------------------------------------------------
331 After the changeset below Test_Isac worked with check_unsynchronized_ref ():
332 ------------------------------------------------------------------------------
333 Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
334 User: Walther Neuper <neuper@ist.tugraz.at>
335 Date: 2012-08-06 10:38:11 +0200 (11 months)
338 The list below records TODOs while producing an ISAC kernel for
339 gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
340 (so to be resumed with Isabelle2013-1):
341 ############## WNxxxxxx.TODO can be found in sources ##############
342 --------------------------------------------------------------------------------
343 WN111013.TODO: lots of cleanup/removal in test/../Test.thy
344 --------------------------------------------------------------------------------
345 WN111013.TODO: remove concept around "fun init_form", lots of troubles with
346 this special case (see) --- why not nxt = Model_Problem here ? ---
347 --------------------------------------------------------------------------------
348 WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
350 # simplify_* , *_simp_*
352 # calc_* , calculate_* ... require iteration over all rls ...
353 ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
354 --------------------------------------------------------------------------------
355 WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
356 --------------------------------------------------------------------------------
357 WN120314 changeset a393bb9f5e9f drops root equations.
358 see test/Tools/isac/Knowledge/rootrateq.sml
359 --------------------------------------------------------------------------------
360 WN120317.TODO changeset 977788dfed26 dropped rateq:
361 # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
362 # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
363 investigation Check_elementwise stopped due to too much effort finding out,
364 why Check_elementwise worked in 2002 in spite of the error.
365 --------------------------------------------------------------------------------
366 WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
367 --------------------------------------------------------------------------------
368 WN120317.TODO found by test --- interSteps for Schalk 299a --- that
369 NO test with 'interSteps' is checked properly (with exn on changed behaviour)
370 --------------------------------------------------------------------------------
371 WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
372 a newly outcommented test where rewrite_set_ make_polynomial --> NONE
373 --------------------------------------------------------------------------------
374 WN120320.TODO check-improve rlsthmsNOTisac:
375 DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
376 DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
377 FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
378 # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
379 --------------------------------------------------------------------------------
380 WN120320.TODO rlsthmsNOTisac: replace twice thms ^
381 --------------------------------------------------------------------------------
382 WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
383 --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
384 --------------------------------------------------------------------------------
385 WN120321.TODO rearrange theories:
389 ///Descript.thy --> ProgLang
390 Delete.thy <--- first_Knowledge_thy (*mv to Atools.thy*)
391 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
392 Interpret.thy are generated (simplifies xml structure for theories)
395 ListC.thy <--- first_Proglang_thy
396 --------------------------------------------------------------------------------
397 WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
398 EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)"
399 broken during work on thy-hierarchy
400 --------------------------------------------------------------------------------
401 WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
402 test --- the_hier (get_thes ()) (collect_thydata ())---
403 --------------------------------------------------------------------------------
404 WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
405 !!add mutual crossreferences to ?fun headline??? where the same has to be done:
406 !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
407 --------------------------------------------------------------------------------
408 WN120409.TODO replace "op mem" (2002) with member (2011) ...
409 ... an exercise interesting for beginners !
410 --------------------------------------------------------------------------------
411 WN120411 scanning html representation of newly generated knowledge:
413 ** Theorems: only "Proof of the theorem" (correct!)
414 and "(c) isac-team (math-autor)"
415 ** Rulesets: only "Identifier:///"
416 and "(c) isac-team (math-autor)"
417 ** IsacKnowledge: link to dependency graph (which needs to be created first)
418 ** IsacScripts --> ProgramLanguage
419 *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
424 ** Z-Transform is missing !!!
425 ** type-constraints !!!
426 --------------------------------------------------------------------------------
427 WN120417: merging xmldata revealed:
428 ..............NEWLY generated:........................................
430 <GUH> thy_isab_Fun-thm-o_apply </GUH>
432 <STRING> Isabelle </STRING>
433 <STRING> Fun </STRING>
434 <STRING> Theorems </STRING>
435 <STRING> o_apply </STRING>
438 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
441 <TEXT> Proof of the theorem </TEXT>
442 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
445 <EXPLANATIONS> </EXPLANATIONS>
447 <STRING> Isabelle team, TU Munich </STRING>
452 ..............OLD FORMAT:.............................................
454 <GUH> thy_isab_Fun-thm-o_apply </GUH>
456 <STRING> Isabelle </STRING>
457 <STRING> Fun </STRING>
458 <STRING> Theorems </STRING>
459 <STRING> o_apply </STRING>
464 <ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
469 <TEXT> Proof of the theorem </TEXT>
470 <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
473 <EXPLANATIONS> </EXPLANATIONS>
475 <STRING> Isabelle team, TU Munich </STRING>
480 --------------------------------------------------------------------------------
482 subsubsection {* Changesets of begin and end *}
484 isac development was done between these changesets:
485 ------------------------------------------------------------------------------
486 Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
487 User: Walther Neuper <neuper@ist.tugraz.at>
488 Date: 2012-09-24 16:39:30 +0200 (8 months)
490 : isac on Isablle2011
492 Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
493 Branch: decompose-isar
494 User: Walther Neuper <neuper@ist.tugraz.at>
495 Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
496 ------------------------------------------------------------------------------
499 subsection {* isac on Isabelle2009-2 *}
500 subsubsection {* Summary of development *}
502 In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
503 The update was painful (bridging 7 years of Isabelle development) and cut short
504 due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
505 going on to Isabelle2011 although most of the tests did not run.
507 subsubsection {* Run tests *}
509 WN131021 this is broken by installation of Isabelle2011/12/13,
510 because all these write their binaries to ~/.isabelle/heaps/..
512 $ cd /usr/local/isabisac09-2/
513 $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
514 $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
515 NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
517 subsubsection {* State of tests *}
519 Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
521 subsubsection {* Changesets of begin and end *}
523 isac development was done between these changesets:
524 ------------------------------------------------------------------------------
525 Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
526 Branch: decompose-isar
527 User: Marco Steger <m.steger@student.tugraz.at>
528 Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
530 : isac on Isablle2009-2
532 Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
533 Branch: isac-from-Isabelle2009-2
534 User: Walther Neuper <neuper@ist.tugraz.at>
535 Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
536 ------------------------------------------------------------------------------
539 subsection {* isac on Isabelle2002 *}
540 subsubsection {* Summary of development *}
542 From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
543 of isac's mathematics engine has been implemented.
545 subsubsection {* Run tests *}
546 subsubsection {* State of tests *}
548 All tests work on an old notebook (the right PolyML coudn't be upgraded to more
549 recent Linux versions)
551 subsubsection {* Changesets of begin and end *}
553 Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
554 see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
558 (*========== inhibit exn 130719 Isabelle2013 ===================================
559 ============ inhibit exn 130719 Isabelle2013 =================================*)
561 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
562 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)