1.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Fri Apr 17 18:47:29 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 11:07:02 2020 +0200
1.3 @@ -122,13 +122,13 @@
1.4 val pats2str' : pat list -> string
1.5 val insert_fillpats: thydata ptyp list -> (pblID * Error_Fill_Def.fillpat list) list -> thydata ptyp list ->
1.6 thydata ptyp list
1.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
1.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.9 val knowthys: unit -> theory list
1.10 (*/------- to Celem4 -------\*)
1.11 val e_pbt: pbt
1.12 (*\------- to Celem4 -------/*)
1.13 val e_met: met
1.14 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.15 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.16
1.17 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
1.18 val overwritelthy: theory -> (Rule_Set.id * (string * Rule_Set.T)) list * (Rule_Set.id * Rule_Set.T) list ->
2.1 --- a/src/Tools/isac/BaseDefinitions/celem-0.sml Fri Apr 17 18:47:29 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/celem-0.sml Sun Apr 19 11:07:02 2020 +0200
2.3 @@ -9,9 +9,9 @@
2.4 sig
2.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.6 (*NONE*)
2.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
2.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.9 (*NONE*)
2.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.12 end
2.13
2.14 (**)
3.1 --- a/src/Tools/isac/BaseDefinitions/celem-1.sml Fri Apr 17 18:47:29 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/celem-1.sml Sun Apr 19 11:07:02 2020 +0200
3.3 @@ -17,9 +17,9 @@
3.4 (*\------- to Celem1 -------/*)
3.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.6 (*NONE*)
3.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
3.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.9 (*NONE*)
3.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.12 end
3.13
3.14 (**)
4.1 --- a/src/Tools/isac/BaseDefinitions/celem-2.sml Fri Apr 17 18:47:29 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/celem-2.sml Sun Apr 19 11:07:02 2020 +0200
4.3 @@ -12,9 +12,9 @@
4.4 (*\------- to Celem2 -------/*)
4.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.6 (*NONE*)
4.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
4.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.9 (*NONE*)
4.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.12 end
4.13
4.14 (**)
5.1 --- a/src/Tools/isac/BaseDefinitions/celem-3.sml Fri Apr 17 18:47:29 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/celem-3.sml Sun Apr 19 11:07:02 2020 +0200
5.3 @@ -20,9 +20,9 @@
5.4 (*\------- to Celem3 -------/*)
5.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.6 (*NONE*)
5.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
5.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.9 (*NONE*)
5.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.12 end
5.13
5.14 (**)
6.1 --- a/src/Tools/isac/BaseDefinitions/celem-4.sml Fri Apr 17 18:47:29 2020 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/celem-4.sml Sun Apr 19 11:07:02 2020 +0200
6.3 @@ -15,9 +15,9 @@
6.4 (*\------- to Celem4 -------/*)
6.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.6 (*NONE*)
6.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
6.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.9 (*NONE*)
6.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.12 end
6.13
6.14 (**)
7.1 --- a/src/Tools/isac/BaseDefinitions/celem-5.sml Fri Apr 17 18:47:29 2020 +0200
7.2 +++ b/src/Tools/isac/BaseDefinitions/celem-5.sml Sun Apr 19 11:07:02 2020 +0200
7.3 @@ -13,9 +13,9 @@
7.4 (*\------- to Celem5 -------/*)
7.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.6 (*NONE*)
7.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
7.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.9 (*NONE*)
7.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.12 end
7.13
7.14 (**)
8.1 --- a/src/Tools/isac/BaseDefinitions/celem-6.sml Fri Apr 17 18:47:29 2020 +0200
8.2 +++ b/src/Tools/isac/BaseDefinitions/celem-6.sml Sun Apr 19 11:07:02 2020 +0200
8.3 @@ -14,9 +14,9 @@
8.4 (*\------- to Celem6 -------/*)
8.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.6 (*NONE*)
8.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
8.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.9 (*NONE*)
8.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.12 end
8.13
8.14 (**)
9.1 --- a/src/Tools/isac/BaseDefinitions/celem-7.sml Fri Apr 17 18:47:29 2020 +0200
9.2 +++ b/src/Tools/isac/BaseDefinitions/celem-7.sml Sun Apr 19 11:07:02 2020 +0200
9.3 @@ -13,9 +13,9 @@
9.4 (*\------- to Celem7 -------/*)
9.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
9.6 (*NONE*)
9.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
9.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.9 (*NONE*)
9.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.12 end
9.13
9.14 (**)
10.1 --- a/src/Tools/isac/BaseDefinitions/celem-8.sml Fri Apr 17 18:47:29 2020 +0200
10.2 +++ b/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 11:07:02 2020 +0200
10.3 @@ -24,9 +24,9 @@
10.4 (*\------- to Celem8 -------/*)
10.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.6 (*NONE*)
10.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
10.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.9 (*NONE*)
10.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.12 end
10.13
10.14 (**)
11.1 --- a/src/Tools/isac/BaseDefinitions/celem-91.sml Fri Apr 17 18:47:29 2020 +0200
11.2 +++ b/src/Tools/isac/BaseDefinitions/celem-91.sml Sun Apr 19 11:07:02 2020 +0200
11.3 @@ -14,9 +14,9 @@
11.4 (*\------- to Celem91 -------/*)
11.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.6 (*NONE*)
11.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
11.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
11.9 (*NONE*)
11.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
11.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
11.12 end
11.13
11.14 (**)
12.1 --- a/src/Tools/isac/BaseDefinitions/celem-92.sml Fri Apr 17 18:47:29 2020 +0200
12.2 +++ b/src/Tools/isac/BaseDefinitions/celem-92.sml Sun Apr 19 11:07:02 2020 +0200
12.3 @@ -9,9 +9,9 @@
12.4 sig
12.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.6 (*NONE*)
12.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
12.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
12.9 (*NONE*)
12.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
12.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
12.12 end
12.13
12.14 (**)
13.1 --- a/src/Tools/isac/BaseDefinitions/celem-93.sml Fri Apr 17 18:47:29 2020 +0200
13.2 +++ b/src/Tools/isac/BaseDefinitions/celem-93.sml Sun Apr 19 11:07:02 2020 +0200
13.3 @@ -9,9 +9,9 @@
13.4 sig
13.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13.6 (*NONE*)
13.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
13.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
13.9 (*NONE*)
13.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13.12 end
13.13
13.14
14.1 --- a/src/Tools/isac/BaseDefinitions/contextC.sml Fri Apr 17 18:47:29 2020 +0200
14.2 +++ b/src/Tools/isac/BaseDefinitions/contextC.sml Sun Apr 19 11:07:02 2020 +0200
14.3 @@ -18,11 +18,11 @@
14.4 (*val subpbl_to_caller .. rename according to naming convention TODO*)
14.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
14.6 (*NONE*)
14.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
14.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
14.9 val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
14.10 val contradict : term list -> term -> bool
14.11 val insert_assumptions_cao : Proof.context -> term list -> Proof.context
14.12 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
14.13 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
14.14 end
14.15
14.16 structure ContextC(**) : CONTEXT_C(**) =
15.1 --- a/src/Tools/isac/BaseDefinitions/error-fill-def.sml Fri Apr 17 18:47:29 2020 +0200
15.2 +++ b/src/Tools/isac/BaseDefinitions/error-fill-def.sml Sun Apr 19 11:07:02 2020 +0200
15.3 @@ -13,9 +13,9 @@
15.4 type fillpat
15.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
15.6 (*NONE*)
15.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
15.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
15.9 (*NONE*)
15.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
15.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
15.12 end
15.13
15.14 (**)
16.1 --- a/src/Tools/isac/BaseDefinitions/exec-def.sml Fri Apr 17 18:47:29 2020 +0200
16.2 +++ b/src/Tools/isac/BaseDefinitions/exec-def.sml Sun Apr 19 11:07:02 2020 +0200
16.3 @@ -15,9 +15,9 @@
16.4 val e_evalfn: Rule_Def.eval_fn
16.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
16.6 (*NONE*)
16.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
16.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
16.9 (*NONE*)
16.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
16.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
16.12 end
16.13
16.14 (**)
17.1 --- a/src/Tools/isac/BaseDefinitions/libraryC.sml Fri Apr 17 18:47:29 2020 +0200
17.2 +++ b/src/Tools/isac/BaseDefinitions/libraryC.sml Sun Apr 19 11:07:02 2020 +0200
17.3 @@ -82,10 +82,10 @@
17.4
17.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
17.6 (* NONE *)
17.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
17.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
17.9 val enumerate_strings: string list -> string list
17.10 val quad2pair: 'a * 'b * 'c * 'd -> 'a * 'b
17.11 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
17.12 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
17.13
17.14
17.15 (*///------------------------------>>> thy ------------------------------------------------\\\*)
18.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml Fri Apr 17 18:47:29 2020 +0200
18.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml Sun Apr 19 11:07:02 2020 +0200
18.3 @@ -19,9 +19,9 @@
18.4 val assoc_rew_ord: string -> subst -> term * term -> bool
18.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
18.6 (*NONE*)
18.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
18.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
18.9 (*NONE*)
18.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
18.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
18.12 end
18.13
18.14 (**)
19.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml Fri Apr 17 18:47:29 2020 +0200
19.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml Sun Apr 19 11:07:02 2020 +0200
19.3 @@ -36,9 +36,9 @@
19.4 (term * term list) option}
19.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
19.6 (*NONE*)
19.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
19.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
19.9 (*NONE*)
19.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
19.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
19.12 end
19.13
19.14 (**)
20.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Fri Apr 17 18:47:29 2020 +0200
20.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Sun Apr 19 11:07:02 2020 +0200
20.3 @@ -31,9 +31,9 @@
20.4
20.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
20.6 (*NONE*)
20.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
20.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
20.9 val insert_merge: for_kestore -> for_kestore list -> for_kestore list
20.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
20.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
20.12 end
20.13
20.14 (**)
21.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Fri Apr 17 18:47:29 2020 +0200
21.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Sun Apr 19 11:07:02 2020 +0200
21.3 @@ -20,9 +20,9 @@
21.4 val thm: rule -> thm
21.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
21.6 val thm_id: rule -> string
21.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
21.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
21.9 (*NONE*)
21.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
21.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
21.12 end
21.13
21.14 (**)
22.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Fri Apr 17 18:47:29 2020 +0200
22.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Sun Apr 19 11:07:02 2020 +0200
22.3 @@ -103,9 +103,9 @@
22.4 val free2var: term -> term
22.5 val contains_one_of: thm * (string * typ) list -> bool
22.6 val contains_Const_typeless: term list -> term -> bool
22.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
22.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
22.9 val typ_a2real: term -> term
22.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
22.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
22.12 end
22.13
22.14 (**)
23.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Fri Apr 17 18:47:29 2020 +0200
23.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Sun Apr 19 11:07:02 2020 +0200
23.3 @@ -17,9 +17,9 @@
23.4 val Isac: 'a -> theory
23.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
23.6 (*NONE*)
23.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
23.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
23.9 val get_thy: id -> theory
23.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
23.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
23.12 end
23.13
23.14 (**)
24.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml Fri Apr 17 18:47:29 2020 +0200
24.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml Sun Apr 19 11:07:02 2020 +0200
24.3 @@ -22,9 +22,9 @@
24.4
24.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
24.6 (*NONE*)
24.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
24.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
24.9 (*NONE*)
24.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
24.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
24.12 end
24.13
24.14 (**)
25.1 --- a/src/Tools/isac/BaseDefinitions/tracing.sml Fri Apr 17 18:47:29 2020 +0200
25.2 +++ b/src/Tools/isac/BaseDefinitions/tracing.sml Sun Apr 19 11:07:02 2020 +0200
25.3 @@ -13,9 +13,9 @@
25.4 (*\------- to Trace from Celem --------/*)
25.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
25.6 (*NONE*)
25.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
25.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
25.9 (*NONE*)
25.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
25.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
25.12 end
25.13
25.14 (**)
26.1 --- a/src/Tools/isac/BaseDefinitions/unparseC.sml Fri Apr 17 18:47:29 2020 +0200
26.2 +++ b/src/Tools/isac/BaseDefinitions/unparseC.sml Sun Apr 19 11:07:02 2020 +0200
26.3 @@ -27,9 +27,9 @@
26.4 val terms: term list -> term_as_string
26.5 val term_by_thyID: ThyC.id -> term -> term_as_string
26.6 val terms_to_strings: term list -> term_as_string list
26.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
26.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
26.9 (*NONE*)
26.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
26.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
26.12 end
26.13
26.14 (**)
27.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Fri Apr 17 18:47:29 2020 +0200
27.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Sun Apr 19 11:07:02 2020 +0200
27.3 @@ -56,9 +56,9 @@
27.4 val setNextTactic : Celem.calcID -> Tactic.input -> XML.tree
27.5 val setProblem : Celem.calcID -> Celem.pblID -> XML.tree
27.6 val setTheory : Celem.calcID -> ThyC.id -> XML.tree
27.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
27.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
27.9 (* NONE *)
27.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
27.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
27.12 end
27.13
27.14 (**)
28.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Apr 17 18:47:29 2020 +0200
28.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Apr 19 11:07:02 2020 +0200
28.3 @@ -44,10 +44,10 @@
28.4 val thydata2xml: Celem.theID * Celem.thydata -> Celem.xml
28.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
28.6 (*NONE*)
28.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
28.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
28.9 val thenode: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Celem.ptyp -> unit
28.10 val thenodes: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Celem.ptyp list -> unit
28.11 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
28.12 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
28.13 end
28.14
28.15 (**)
29.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Fri Apr 17 18:47:29 2020 +0200
29.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Sun Apr 19 11:07:02 2020 +0200
29.3 @@ -25,7 +25,7 @@
29.4 val rule2rls' : Rule.rule -> string
29.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
29.6 (* NONE *)
29.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
29.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
29.9 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
29.10 val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
29.11 val check_err_patt : term * term -> UnparseC.subst -> Error_Fill_Def.errpatID * term -> Rule_Set.T -> Error_Fill_Def.errpatID option
29.12 @@ -33,7 +33,7 @@
29.13 'a * (term * term) list -> 'b * term -> Error_Fill_Def.errpatID -> Error_Fill_Def.fillpat -> (Error_Fill_Def.fillpatID * term * 'b * 'a) option
29.14 val get_fillpats :
29.15 'a * (term * term) list -> term -> Error_Fill_Def.errpatID -> thm -> (Error_Fill_Def.fillpatID * term * thm * 'a) list
29.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
29.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
29.18
29.19 end
29.20 (**)
30.1 --- a/src/Tools/isac/Interpret/li-tool.sml Fri Apr 17 18:47:29 2020 +0200
30.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Sun Apr 19 11:07:02 2020 +0200
30.3 @@ -26,9 +26,9 @@
30.4 Program.leaf * term option
30.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
30.6 (*NONE*)
30.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
30.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
30.9 val arguments_from_model : Celem.metID -> Model.itm list -> term list
30.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
30.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
30.12 end
30.13
30.14 (* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step *)
31.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Fri Apr 17 18:47:29 2020 +0200
31.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sun Apr 19 11:07:02 2020 +0200
31.3 @@ -44,7 +44,7 @@
31.4 val go_scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> expr_val
31.5 val scan_to_tactic: term * (Calc.T * Proof.context) -> Istate.T -> expr_val
31.6 val check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option -> expr_val
31.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
31.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
31.9 val check_Let_up: Istate.pstate -> term -> term * term
31.10 val compare_step: Generate.taci list * Pos.pos' list * (Calc.T) -> term -> string * Chead.calcstate'
31.11
31.12 @@ -54,7 +54,7 @@
31.13 val scan_to_tactic1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.T -> expr_val1
31.14
31.15 val check_tac1: Calc.T * Proof.context * Tactic.T -> Istate.pstate -> term * term option -> expr_val1
31.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
31.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
31.18 end
31.19
31.20 (**)
32.1 --- a/src/Tools/isac/Interpret/rewtools.sml Fri Apr 17 18:47:29 2020 +0200
32.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Sun Apr 19 11:07:02 2020 +0200
32.3 @@ -43,12 +43,12 @@
32.4 val guh2theID : Celem.guh -> Celem.theID
32.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
32.6 (* NONE *)
32.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
32.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
32.9 val trtas2str : (term * Rule.rule * (term * term list)) list -> string
32.10 val eq_Thm : Rule.rule * Rule.rule -> bool
32.11 val deriv2str : (term * Rule.rule * (term * term list)) list -> string
32.12 val deriv_of_thm'' : ThmC.T -> string
32.13 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
32.14 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
32.15
32.16 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
32.17 val deri2str : (Rule.rule * (term * term list)) list -> string
33.1 --- a/src/Tools/isac/Interpret/sub-problem.sml Fri Apr 17 18:47:29 2020 +0200
33.2 +++ b/src/Tools/isac/Interpret/sub-problem.sml Sun Apr 19 11:07:02 2020 +0200
33.3 @@ -4,9 +4,9 @@
33.4 val tac_from_prog: Ctree.ctree -> term -> Tactic.input * Tactic.T
33.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
33.6 (*NONE*)
33.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
33.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
33.9 (*NONE*)
33.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
33.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
33.12 end
33.13
33.14 (**)
34.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Fri Apr 17 18:47:29 2020 +0200
34.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Sun Apr 19 11:07:02 2020 +0200
34.3 @@ -39,13 +39,13 @@
34.4 (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option -> CTbasic.ctree
34.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
34.6 (*NONE*)
34.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
34.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
34.9 val append_form: Pos.pos -> Istate_Def.T * Proof.context -> term -> CTbasic.ctree -> CTbasic.ctree
34.10 val append_problem : Pos.pos -> Istate_Def.T * Proof.context -> Selem.fmz ->
34.11 Model.ori list * Celem.spec * term * Proof.context -> CTbasic.ctree -> CTbasic.ctree
34.12 val update_problem: Pos.pos -> Celem.spec * Model.itm list * Model.itm list * Proof.context
34.13 -> CTbasic.ctree -> CTbasic.ctree
34.14 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
34.15 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
34.16 end
34.17 (**)
34.18 structure CTaccess(**): CALC_TREE_ACCESS(**) =
35.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Fri Apr 17 18:47:29 2020 +0200
35.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Sun Apr 19 11:07:02 2020 +0200
35.3 @@ -101,7 +101,7 @@
35.4 val par_pblobj : CTbasic.ctree -> Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *)
35.5 ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
35.6
35.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
35.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
35.9 val pr_ctree : (Pos.pos -> ppobj -> string) -> ctree -> string
35.10 val pr_short : Pos.pos -> ppobj -> string
35.11 val g_ctxt : ppobj -> Proof.context
35.12 @@ -115,7 +115,7 @@
35.13 val cut_level_'_ : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list
35.14 val get_trace : ctree -> int list -> int list -> int list list
35.15 val branch2str : branch -> string
35.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
35.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
35.18
35.19 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
35.20 (* NONE *)
36.1 --- a/src/Tools/isac/MathEngBasic/ctree-navi.sml Fri Apr 17 18:47:29 2020 +0200
36.2 +++ b/src/Tools/isac/MathEngBasic/ctree-navi.sml Sun Apr 19 11:07:02 2020 +0200
36.3 @@ -19,9 +19,9 @@
36.4
36.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
36.6 (* NONE *)
36.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
36.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
36.9 (* NONE *)
36.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
36.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
36.12
36.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
36.14 (* NONE *)
37.1 --- a/src/Tools/isac/MathEngBasic/ctree.sml Fri Apr 17 18:47:29 2020 +0200
37.2 +++ b/src/Tools/isac/MathEngBasic/ctree.sml Sun Apr 19 11:07:02 2020 +0200
37.3 @@ -30,10 +30,10 @@
37.4
37.5
37.6 end;
37.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
37.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
37.9 open Ctree;
37.10 open Pos
37.11 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
37.12 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
37.13
37.14 (* policy for "open" structures:
37.15 --------------------------------
38.1 --- a/src/Tools/isac/MathEngBasic/model.sml Fri Apr 17 18:47:29 2020 +0200
38.2 +++ b/src/Tools/isac/MathEngBasic/model.sml Sun Apr 19 11:07:02 2020 +0200
38.3 @@ -51,9 +51,9 @@
38.4 val penv2str_ : Proof.context -> penv -> string (* NONE *)
38.5 type preori
38.6 val preoris2str : preori list -> string
38.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
38.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
38.9 (* NONE *)
38.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
38.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
38.12
38.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
38.14 val untouched : itm list -> bool
39.1 --- a/src/Tools/isac/MathEngBasic/mstools.sml Fri Apr 17 18:47:29 2020 +0200
39.2 +++ b/src/Tools/isac/MathEngBasic/mstools.sml Sun Apr 19 11:07:02 2020 +0200
39.3 @@ -20,9 +20,9 @@
39.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
39.5 val pres2str : (bool * term) list -> string
39.6 val refined : match list -> Celem.pblID
39.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
39.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
39.9 (*NONE*)
39.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
39.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
39.12
39.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
39.14 val pblID_of_match : match -> Celem.pblID
40.1 --- a/src/Tools/isac/MathEngBasic/position.sml Fri Apr 17 18:47:29 2020 +0200
40.2 +++ b/src/Tools/isac/MathEngBasic/position.sml Sun Apr 19 11:07:02 2020 +0200
40.3 @@ -33,8 +33,8 @@
40.4
40.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
40.6 val pos's2str: pos' list -> string
40.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
40.8 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
40.9 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
40.10 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
40.11 end
40.12
40.13 (**)
41.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Fri Apr 17 18:47:29 2020 +0200
41.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Sun Apr 19 11:07:02 2020 +0200
41.3 @@ -21,14 +21,14 @@
41.4 -> term -> (term * term list) option
41.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
41.6 (* NONE *)
41.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
41.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
41.9 val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
41.10 Rule_Set.T -> bool -> thm -> term -> (term * term list) option
41.11 val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
41.12 val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
41.13 val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
41.14 val trace1: int -> string -> unit
41.15 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
41.16 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
41.17 end
41.18
41.19 (**)
42.1 --- a/src/Tools/isac/MathEngBasic/specification-elems.sml Fri Apr 17 18:47:29 2020 +0200
42.2 +++ b/src/Tools/isac/MathEngBasic/specification-elems.sml Sun Apr 19 11:07:02 2020 +0200
42.3 @@ -33,9 +33,9 @@
42.4 val e_sube : TermC.as_string list
42.5 val e_subs : string list
42.6 val subte2subst : term list -> (term * term) list
42.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
42.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
42.9 (* NONE *)
42.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
42.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
42.12
42.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
42.14 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
43.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 17 18:47:29 2020 +0200
43.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Sun Apr 19 11:07:02 2020 +0200
43.3 @@ -122,9 +122,9 @@
43.4
43.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
43.6 (* NONE *)
43.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
43.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
43.9 (* NONE *)
43.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
43.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
43.12
43.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
43.14 (* NONE *)
44.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Fri Apr 17 18:47:29 2020 +0200
44.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Sun Apr 19 11:07:02 2020 +0200
44.3 @@ -28,9 +28,9 @@
44.4 val id_drop_sym: id -> id
44.5 val make_sym_rule: Rule.rule -> Rule.rule
44.6 val make_sym_rule_set: Rule_Set.T -> Rule_Set.T
44.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
44.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
44.9 val sym_thm: thm -> thm
44.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
44.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
44.12 end
44.13
44.14 (**)
45.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Fri Apr 17 18:47:29 2020 +0200
45.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Sun Apr 19 11:07:02 2020 +0200
45.3 @@ -20,9 +20,9 @@
45.4 val tryrefine : Celem.pblID -> Ctree.ctree -> Pos.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
45.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
45.6 (*NONE*)
45.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
45.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
45.9 (*NONE*)
45.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
45.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
45.12
45.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
45.14 (* NONE *)
46.1 --- a/src/Tools/isac/MathEngine/solve.sml Fri Apr 17 18:47:29 2020 +0200
46.2 +++ b/src/Tools/isac/MathEngine/solve.sml Sun Apr 19 11:07:02 2020 +0200
46.3 @@ -16,9 +16,9 @@
46.4
46.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
46.6 (*NONE*)
46.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
46.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
46.9 (*NONE*)
46.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
46.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
46.12
46.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
46.14 (* NONE *)
47.1 --- a/src/Tools/isac/MathEngine/step.sml Fri Apr 17 18:47:29 2020 +0200
47.2 +++ b/src/Tools/isac/MathEngine/step.sml Sun Apr 19 11:07:02 2020 +0200
47.3 @@ -22,10 +22,10 @@
47.4
47.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
47.6 (*NONE*)
47.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
47.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
47.9 val specify_do_next: Calc.T -> string * Chead.calcstate'
47.10 val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Chead.calcstate'
47.11 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
47.12 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
47.13 end
47.14
47.15 (**)
48.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Fri Apr 17 18:47:29 2020 +0200
48.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Sun Apr 19 11:07:02 2020 +0200
48.3 @@ -37,7 +37,7 @@
48.4 val gen: theory -> term -> Rule_Set.T -> term
48.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
48.6 (* NONE *)
48.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
48.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
48.9 val subst_typ: string -> typ -> term list -> (typ * typ) list
48.10 val is_calc: term -> bool
48.11 val rule2stac: theory -> Rule.rule -> term
48.12 @@ -45,7 +45,7 @@
48.13 val #> : term list -> term
48.14 val rules2scr_Rls : theory -> Rule.rule list -> term
48.15 val rules2scr_Seq : theory -> Rule.rule list -> term
48.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
48.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
48.18 end
48.19 (**)
48.20 structure Auto_Prog(**): AUTO_GERNERATE_PROGRAM(**) =
49.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Fri Apr 17 18:47:29 2020 +0200
49.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Apr 19 11:07:02 2020 +0200
49.3 @@ -87,9 +87,9 @@
49.4 (*\\------------------------- from Atools.thy------------------------------------------------//*)
49.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
49.6 (*NONE*)
49.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
49.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
49.9 (*NONE*)
49.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
49.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
49.12 end
49.13
49.14 (**)
50.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Fri Apr 17 18:47:29 2020 +0200
50.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Sun Apr 19 11:07:02 2020 +0200
50.3 @@ -63,9 +63,9 @@
50.4 val is: term -> bool
50.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
50.6 (*NONE*)
50.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
50.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
50.9 (*NONE*)
50.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
50.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
50.12 end
50.13 \<close> ML \<open>
50.14 (**)
51.1 --- a/src/Tools/isac/ProgLang/Program.thy Fri Apr 17 18:47:29 2020 +0200
51.2 +++ b/src/Tools/isac/ProgLang/Program.thy Sun Apr 19 11:07:02 2020 +0200
51.3 @@ -46,9 +46,9 @@
51.4 val to_string: Rule_Def.program -> string
51.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
51.6 (* NONE *)
51.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
51.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
51.9 (* NONE *)
51.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
51.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
51.12 end
51.13 \<close> ML \<open>
51.14 \<close> ML \<open>
52.1 --- a/src/Tools/isac/ProgLang/Tactical.thy Fri Apr 17 18:47:29 2020 +0200
52.2 +++ b/src/Tools/isac/ProgLang/Tactical.thy Sun Apr 19 11:07:02 2020 +0200
52.3 @@ -28,9 +28,9 @@
52.4
52.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
52.6 (*NONE*)
52.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
52.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
52.9 (*NONE*)
52.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
52.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
52.12 end
52.13
52.14 \<close> ML \<open>
53.1 --- a/src/Tools/isac/ProgLang/calculate.sml Fri Apr 17 18:47:29 2020 +0200
53.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Sun Apr 19 11:07:02 2020 +0200
53.3 @@ -22,12 +22,12 @@
53.4 val float_op_var: term -> string -> typ -> typ -> float -> term
53.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
53.6 (* NONE *)
53.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
53.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
53.9 val get_pair: theory -> string -> Exec_Def.eval_fn -> term -> (string * term) option
53.10 val mk_rule: term list * term * term -> term
53.11 val divisors: int -> int list
53.12 val doubles: int list -> int list
53.13 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
53.14 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
53.15 end
53.16
53.17 (**)
54.1 --- a/src/Tools/isac/Specify/Input_Descript.thy Fri Apr 17 18:47:29 2020 +0200
54.2 +++ b/src/Tools/isac/Specify/Input_Descript.thy Sun Apr 19 11:07:02 2020 +0200
54.3 @@ -71,9 +71,9 @@
54.4 val pbl_ids: Proof.context -> term -> term -> term list
54.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
54.6 (* NONE *)
54.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
54.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
54.9 (* NONE *)
54.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
54.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
54.12 end
54.13 \<close> ML \<open>
54.14 (**)
55.1 --- a/src/Tools/isac/Specify/appl.sml Fri Apr 17 18:47:29 2020 +0200
55.2 +++ b/src/Tools/isac/Specify/appl.sml Sun Apr 19 11:07:02 2020 +0200
55.3 @@ -11,9 +11,9 @@
55.4 val applicable_in : Pos.pos' -> Ctree.ctree -> Tactic.input -> appl
55.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
55.6 val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T
55.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
55.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
55.9 val mk_set : 'a -> ctree -> pos -> term -> term -> term * term list
55.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
55.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
55.12 end
55.13
55.14 (**)
56.1 --- a/src/Tools/isac/Specify/calchead.sml Fri Apr 17 18:47:29 2020 +0200
56.2 +++ b/src/Tools/isac/Specify/calchead.sml Sun Apr 19 11:07:02 2020 +0200
56.3 @@ -110,7 +110,7 @@
56.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
56.5 val e_calcstate : Calc.T * Generate.taci list
56.6 val e_calcstate' : calcstate'
56.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
56.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
56.9 val posterms2str : (Pos.pos' * term * 'a) list -> string
56.10 val postermtacs2str : (Pos.pos' * term * Tactic.input option) list -> string
56.11 val is_copy_named_idstr : string -> bool
56.12 @@ -125,7 +125,7 @@
56.13 val appl_add: Proof.context -> string -> Model.ori list ->
56.14 Model.itm list -> (string * (term * term)) list -> TermC.as_string -> additm
56.15 val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
56.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
56.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
56.18
56.19 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
56.20 val variants_in : term list -> int
57.1 --- a/src/Tools/isac/Specify/generate.sml Fri Apr 17 18:47:29 2020 +0200
57.2 +++ b/src/Tools/isac/Specify/generate.sml Sun Apr 19 11:07:02 2020 +0200
57.3 @@ -29,10 +29,10 @@
57.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
57.5 val tacis2str : taci list -> string
57.6 val mout2str : mout -> string
57.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
57.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
57.9 val res_from_taci : taci -> (term * term list)
57.10 val insert_pos : Pos.pos -> taci list -> taci list
57.11 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
57.12 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
57.13
57.14 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
57.15 (* NONE *)
58.1 --- a/src/Tools/isac/Specify/input-calchead.sml Fri Apr 17 18:47:29 2020 +0200
58.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Sun Apr 19 11:07:02 2020 +0200
58.3 @@ -12,9 +12,9 @@
58.4 val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
58.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
58.6 (* NONE *)
58.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
58.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
58.9 (* NONE *)
58.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
58.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
58.12
58.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
58.14 val e_icalhd : icalhd
59.1 --- a/src/Tools/isac/Specify/ptyps.sml Fri Apr 17 18:47:29 2020 +0200
59.2 +++ b/src/Tools/isac/Specify/ptyps.sml Sun Apr 19 11:07:02 2020 +0200
59.3 @@ -58,7 +58,7 @@
59.4 val e_errpat : Error_Fill_Def.errpat
59.5 val show_pblguhs : unit -> unit
59.6 val sort_pblguhs : unit -> unit
59.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
59.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
59.9 val add_field : theory -> Celem.pat list -> term * 'b -> string * term * 'b
59.10 val add_variants : ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
59.11 val coll_variants: ('a * ''b) list -> ('a list * ''b) list
59.12 @@ -66,7 +66,7 @@
59.13 val max: int list -> int
59.14 val replace_0: int -> int list -> int list
59.15 val split_did: term -> term * term
59.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
59.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
59.18
59.19 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
59.20 val e_fillpat : string * term * string
60.1 --- a/src/Tools/isac/Specify/specify.sml Fri Apr 17 18:47:29 2020 +0200
60.2 +++ b/src/Tools/isac/Specify/specify.sml Sun Apr 19 11:07:02 2020 +0200
60.3 @@ -4,9 +4,9 @@
60.4 val nxt_specify_init_calc : Selem.fmz -> Chead.calcstate
60.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
60.6 (*NONE*)
60.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
60.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
60.9 (*NONE*)
60.10 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
60.11 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
60.12 end
60.13
60.14 (**)
61.1 --- a/src/Tools/isac/Specify/step-specify.sml Fri Apr 17 18:47:29 2020 +0200
61.2 +++ b/src/Tools/isac/Specify/step-specify.sml Sun Apr 19 11:07:02 2020 +0200
61.3 @@ -11,8 +11,8 @@
61.4 (* ---- keep, probably required later in devel. ----------------------------------------------- *)
61.5 val nxt_specify_init_calc: Selem.fmz
61.6 -> Calc.T * (Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))) list
61.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
61.8 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
61.9 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
61.10 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
61.11
61.12 end
61.13
62.1 --- a/src/Tools/isac/TODO.thy Fri Apr 17 18:47:29 2020 +0200
62.2 +++ b/src/Tools/isac/TODO.thy Sun Apr 19 11:07:02 2020 +0200
62.3 @@ -50,19 +50,13 @@
62.4 \<close>
62.5 subsection \<open>Postponed from current changeset\<close>
62.6 text \<open>
62.7 - \item "TODO CLEANUP Thm"
62.8 - (* TODO CLEANUP Thm:
62.9 - Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
62.10 - thmID : type for data from user input + program
62.11 - thmDeriv : type for thy_hierarchy ONLY
62.12 - obsolete types : thm' (SEE "ad thm'"), thm''.
62.13 - revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
62.14 - activate : ThmC.cut_id'
62.15 - *)
62.16 + \begin{itemize}
62.17 + \item xxx
62.18 + \item xxx
62.19 \item xxx
62.20 \item use "Exec_Def" for renaming identifiers
62.21 \item xxx
62.22 - \item xxx
62.23 + \item why does Test_Build_Thydata.thy depend on ProgLang and not on CalcElements ?
62.24 \item xxx
62.25 \item xxx
62.26 \begin{itemize}
62.27 @@ -610,6 +604,33 @@
62.28 \begin{itemize}
62.29 \item ad ERROR Undefined fact "all_left" in Test_Isac: error-pattern.sml
62.30 Undefined fact: "xfoldr_Nil" inssort.sml
62.31 + (* probably two different reasons:
62.32 + src/../LinEq.thy
62.33 + (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
62.34 + all_left: "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
62.35 +
62.36 + src/../PolyEq.thy
62.37 + (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
62.38 + all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and
62.39 +
62.40 + test/../partial_fractions.sml
62.41 + (*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
62.42 + (*[7, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"))*)
62.43 +
62.44 + test/../mathengine-stateless.sml
62.45 + (*if ThmC.string_of_thm @ {thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
62.46 + then () else error "string_of_thm changed";*)
62.47 +
62.48 + (*---------------------------------------------------------------------------------------------*)
62.49 + src/../LinEq.thy
62.50 + primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
62.51 + xfoldr_Nil: "xfoldr f {|| ||} = id" |
62.52 + xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
62.53 +
62.54 + src/../InsSort.thy
62.55 + srls = Rule_Set.empty, calc = [], rules = [
62.56 + Rule.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
62.57 + *)
62.58 \item xxx
62.59 \item xxx
62.60 \item ?OK Test_Isac_Short with
63.1 --- a/test/Tools/isac/Test_Isac_Short.thy Fri Apr 17 18:47:29 2020 +0200
63.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sun Apr 19 11:07:02 2020 +0200
63.3 @@ -152,8 +152,8 @@
63.4 \<close> ML \<open>
63.5 \<close> ML \<open>
63.6 \<close> ML \<open>
63.7 -\<close> ML \<open>
63.8 -\<close> ML \<open>
63.9 +\<close> ML \<open>`
63.10 +\<close> ML \<open>`
63.11 \<close> ML \<open>
63.12 \<close> ML \<open>
63.13 \<close> ML \<open>
64.1 --- a/test/Tools/isac/Test_Some.thy Fri Apr 17 18:47:29 2020 +0200
64.2 +++ b/test/Tools/isac/Test_Some.thy Sun Apr 19 11:07:02 2020 +0200
64.3 @@ -96,6 +96,9 @@
64.4 section \<open>===================================================================================\<close>
64.5 ML \<open>
64.6 \<close> ML \<open>
64.7 +val (Const ("HOL.Not", _) $ xxx) = @{term "Not (a = b)"}
64.8 +\<close> ML \<open>
64.9 +@{thm all_left}
64.10 \<close> ML \<open>
64.11 \<close>
64.12