1.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Sun Aug 28 12:32:57 2016 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Thu Sep 08 13:28:36 2016 +0200
     1.3 @@ -22,12 +22,12 @@
     1.4  subsection {* functions *}
     1.5  primrec ins :: "int \<Rightarrow> int xlist \<Rightarrow> int xlist"
     1.6  where
     1.7 -ins_Nil:  "ins i [|| ||] = [||i||]" |
     1.8 +ins_Nil:  "ins i {|| ||} = {||i||}" |
     1.9  ins_Cons: "ins i (x @# xs) = (if i < x then (i @# x @# xs) else x @# (ins i xs))"
    1.10  
    1.11  fun sort :: "int xlist \<Rightarrow> int xlist"
    1.12  where
    1.13 -sort_deff: "sort xs = xfoldr ins xs [|| ||]"
    1.14 +sort_deff: "sort xs = xfoldr ins xs {|| ||}"
    1.15  print_theorems
    1.16  thm sort_def  (* InsSort.sort \<equiv> sort_sumC *)
    1.17  thm sort_deff (* InsSort.sort ?xs = foldr ins ?xs [] *)
    1.18 @@ -38,8 +38,8 @@
    1.19  @{thm ins.simps(2)};
    1.20  *}
    1.21  
    1.22 -value "sort [||2,3,1||]"
    1.23 -lemma test: "sort [||2,3,1||] = [||1,2,3||]"
    1.24 +value "sort {||2,3,1||}"
    1.25 +lemma test: "sort {||2,3,1||} = {||1,2,3||}"
    1.26  by simp
    1.27  
    1.28  subsection {* eval functions *}
    1.29 @@ -108,7 +108,7 @@
    1.30  
    1.31  subsection {* CAS-commands *}
    1.32  ML {*
    1.33 -(* for starting a new example, e.g. "Sort [|| 1, 3, 2 ||]" after <NEW> on WorkSheet;
    1.34 +(* for starting a new example, e.g. "Sort {|| 1, 3, 2 ||}" after <NEW> on WorkSheet;
    1.35     associate above input with dataformat of pbt (without "#Given", etc):
    1.36  *)
    1.37  fun argl2dtss [t] =

     2.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Sun Aug 28 12:32:57 2016 +0200
     2.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Thu Sep 08 13:28:36 2016 +0200
     2.3 @@ -39,19 +39,19 @@
     2.4  subsection {* Type 'xlist' for Lucas-Interpretation *}
     2.5  (*TODO: ask for shorter deliminters in xlist *)
     2.6  datatype 'a xlist =
     2.7 -    XNil    ("[|| ||]")
     2.8 +    XNil    ("{|| ||}")
     2.9    | XCons 'a  "'a xlist"    (infixr "@#" 65)
    2.10  
    2.11  syntax
    2.12    -- {* list Enumeration *}
    2.13 -  "_xlist" :: "args => 'a xlist"    ("[||(_)||]")
    2.14 +  "_xlist" :: "args => 'a xlist"    ("{|| (_) ||}")
    2.15  
    2.16  translations
    2.17 -  "[||x, xs||]" == "x@#[||xs||]"
    2.18 -  "[||x||]" == "x@#[|| ||]"
    2.19 +  "{||x, xs||}" == "x@#{||xs||}"
    2.20 +  "{||x||}" == "x@#{|| ||}"
    2.21  
    2.22 -term "[|| ||]"
    2.23 -term "[||1,2,3||]"
    2.24 +term "{|| ||}"
    2.25 +term "{||1,2,3||}"
    2.26  
    2.27  subsection {* Functions for 'xlist' *}
    2.28  (* TODO: 
    2.29 @@ -62,7 +62,7 @@
    2.30  *)
    2.31  
    2.32  primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
    2.33 -xfoldr_Nil:  "xfoldr f [|| ||] = id" |
    2.34 +xfoldr_Nil:  "xfoldr f {|| ||} = id" |
    2.35  xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
    2.36  
    2.37  primrec LENGTH   :: "'a list => real"

     3.1 --- a/test/Tools/isac/Knowledge/inssort.sml	Sun Aug 28 12:32:57 2016 +0200
     3.2 +++ b/test/Tools/isac/Knowledge/inssort.sml	Thu Sep 08 13:28:36 2016 +0200
     3.3 @@ -31,70 +31,70 @@
     3.4  "----------- insertion sort by rewrite stepwise ------------------------------";
     3.5  "----------- insertion sort by rewrite stepwise ------------------------------";
     3.6  val ctxt = Proof_Context.init_global @{theory};
     3.7 -val SOME t = parseNEW ctxt "sort [||1, 3, 2||]";
     3.8 +val SOME t = parseNEW ctxt "sort {|| 1, 3, 2 ||}";
     3.9  
    3.10  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm sort_deff} t;
    3.11 -term2str t' (*"foldr ins [1, 3, 2] []"*);
    3.12 +term2str t' = "xfoldr ins {|| 1, 3, 2 ||} {|| ||}";
    3.13  
    3.14  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Cons} t';
    3.15 -term2str t' (*"(ins 1 o foldr ins [3, 2]) []"*);
    3.16 +term2str t' = "(ins 1 o xfoldr ins {|| 3, 2 ||}) {|| ||}";
    3.17  
    3.18  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Cons} t';
    3.19 -term2str t' (*"(ins 1 o (ins 3 o foldr ins [2])) []"*);
    3.20 +term2str t' = "(ins 1 o (ins 3 o xfoldr ins {|| 2 ||})) {|| ||}";
    3.21  
    3.22  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Cons} t';
    3.23 -term2str t' (*"(ins 1 o (ins 3 o (ins 2 o foldr ins []))) []"*);
    3.24 +term2str t' = "(ins 1 o (ins 3 o (ins 2 o xfoldr ins {|| ||}))) {|| ||}";
    3.25  
    3.26  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm xfoldr_Nil} t';
    3.27 -term2str t' (*"(ins 1 o (ins 3 o (ins 2 o id))) []"*);
    3.28 +term2str t' = "(ins 1 o (ins 3 o (ins 2 o id))) {|| ||}";
    3.29  
    3.30  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_id} t';
    3.31 -term2str t' (*"(ins 1 o (ins 3 o ins 2)) []"*);
    3.32 +term2str t' = "(ins 1 o (ins 3 o ins 2)) {|| ||}";
    3.33  
    3.34  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_assoc} t';
    3.35 -term2str t' (*"(ins 1 o ins 3 o ins 2) []" = "((ins 1 o ins 3) o ins 2) []"*);
    3.36 +term2str t' = "(ins 1 o ins 3 o ins 2) {|| ||}";
    3.37  
    3.38  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_apply} t';
    3.39 -term2str t' (*"(ins 1 o ins 3) (ins 2 [])"*);
    3.40 +term2str t' = "(ins 1 o ins 3) (ins 2 {|| ||})";
    3.41  
    3.42  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm o_apply} t';
    3.43 -term2str t' (*"ins 1 (ins 3 (ins 2 []))"*);
    3.44 +term2str t' = "ins 1 (ins 3 (ins 2 {|| ||}))";
    3.45  
    3.46  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Nil} t';
    3.47 -term2str t' (*"ins 1 (ins 3 [2])"*);
    3.48 +term2str t' = "ins 1 (ins 3 {|| 2 ||})";
    3.49  
    3.50  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Cons} t';
    3.51 -term2str t' (*"ins 1 (if 3 < 2 then [3, 2] else 2 # ins 3 [])"*);
    3.52 +term2str t' = "ins 1 (if 3 < 2 then {|| 3, 2 ||} else 2 @# ins 3 {|| ||})";
    3.53  
    3.54  val SOME (t', _) = calculate_ @{theory} ("Orderings.ord_class.less", eval_equ "#less_")  t';
    3.55 -term2str t' (*"ins 1 (if False then [3, 2] else 2 # ins 3 [])"*);
    3.56 +term2str t' = "ins 1 (if False then {|| 3, 2 ||} else 2 @# ins 3 {|| ||})";
    3.57  
    3.58  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm if_False} t';
    3.59 -term2str t' (*"ins 1 (2 # ins 3 [])"*);
    3.60 +term2str t' = "ins 1 (2 @# ins 3 {|| ||})";
    3.61  
    3.62  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Nil} t';
    3.63 -term2str t' (*"ins 1 [2, 3]"*);
    3.64 +term2str t' = "ins 1 {|| 2, 3 ||}";
    3.65  
    3.66  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm ins_Cons} t';
    3.67 -term2str t' (*"if 1 < 2 then [1, 2, 3] else 2 # ins 1 [3]"*);
    3.68 +term2str t' = "if 1 < 2 then {|| 1, 2, 3 ||} else 2 @# ins 1 {|| 3 ||}";
    3.69  
    3.70  val SOME (t', _) = calculate_ @{theory} ("Orderings.ord_class.less", eval_equ "#less_")  t';
    3.71 -term2str t' (*"if True then [1, 2, 3] else 2 # ins 1 [3]"*);
    3.72 +term2str t' = "if True then {|| 1, 2, 3 ||} else 2 @# ins 1 {|| 3 ||}";
    3.73  
    3.74  val SOME (t', _) = rewrite_ @{theory} tless_true eval_rls false @{thm if_True} t';
    3.75 -if term2str t' = "[||1, 2, 3||]" then () else error "CHANGED RESULT FOR sort by rewrite stepwise";
    3.76 +if term2str t' = "{|| 1, 2, 3 ||}" then () else error "CHANGED RESULT FOR sort by rewrite stepwise";
    3.77  
    3.78  "----------- insertion sort with ruleset -------------------------------------";
    3.79  "----------- insertion sort with ruleset -------------------------------------";
    3.80  "----------- insertion sort with ruleset -------------------------------------";
    3.81 -if term2str t = "InsSort.sort [||1, 3, 2||]" then () else error "CHANGED START FOR sort with ruleset";
    3.82 +if term2str t = "InsSort.sort {|| 1, 3, 2 ||}" then () else error "CHANGED START FOR sort with ruleset";
    3.83  val SOME (t', _) = rewrite_set_ @{theory} false ins_sort t;
    3.84 -if term2str t' = "[||1, 2, 3||]" then () else error "CHANGED RESULT FOR sort with ruleset";
    3.85 +if term2str t' = "{|| 1, 2, 3 ||}" then () else error "CHANGED RESULT FOR sort with ruleset";
    3.86  
    3.87  "----------- insertion sort with MathEngine ----------------------------------";
    3.88  "----------- insertion sort with MathEngine ----------------------------------";
    3.89  "----------- insertion sort with MathEngine ----------------------------------";
    3.90 -val fmz = ["unsorted [||1, 3, 2||]", "sorted s_s"];
    3.91 +val fmz = ["unsorted {||1, 3, 2||}", "sorted s_s"];
    3.92  val (dI',pI',mI') = ("InsSort", ["insertion","sort","Programming"], 
    3.93    ["Programming","sort","insertion"]);
    3.94  val p = e_pos'; val c = []; 
    3.95 @@ -108,18 +108,18 @@
    3.96  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    3.97  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    3.98  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    3.99 -if nxt = ("End_Proof'", End_Proof') andalso f2str f = "[||1, 2, 3||]" then ()
   3.100 +if nxt = ("End_Proof'", End_Proof') andalso f2str f = "{|| 1, 2, 3 ||}" then ()
   3.101  else error "--- insertion sort with MathEngine CHANGED"
   3.102  
   3.103  "----------- insertion sort: CAS-command -------------------------------------";
   3.104  "----------- insertion sort: CAS-command -------------------------------------";
   3.105  "----------- insertion sort: CAS-command -------------------------------------";
   3.106  val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
   3.107 -val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "Sort [||1, 3, 2||]";
   3.108 +val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "Sort {||1, 3, 2||}";
   3.109  show_pt pt;
   3.110  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method",..*)
   3.111  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* nxt = ("Rewrite_Set",..*)
   3.112  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* nxt = ("Check_Postcond",..*)
   3.113  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* nxt = ("End_Proof'",..*)
   3.114 -if nxt = ("End_Proof'", End_Proof') andalso f2str f = "[||1, 2, 3||]" then ()
   3.115 +if nxt = ("End_Proof'", End_Proof') andalso f2str f = "{|| 1, 2, 3 ||}" then ()
   3.116  else error "--- insertion sort: CAS-command CHANGED"

     4.1 --- a/test/Tools/isac/ProgLang/listC.sml	Sun Aug 28 12:32:57 2016 +0200
     4.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Thu Sep 08 13:28:36 2016 +0200
     4.3 @@ -7,34 +7,34 @@
     4.4  "-----------------------------------------------------------------------------";
     4.5  "table of contents -----------------------------------------------------------";
     4.6  "-----------------------------------------------------------------------------";
     4.7 -"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
     4.8 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
     4.9  "--------------------- NTH ---------------------------------------------------";
    4.10  "--------------------- LENGTH ------------------------------------------------";
    4.11  "--------------------- tl ----------------------------------------------------";
    4.12  "-----------------------------------------------------------------------------";
    4.13  "-----------------------------------------------------------------------------";
    4.14  
    4.15 -"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
    4.16 -"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
    4.17 -"----------- check 'type xlist' [||1, 2, 3||] --------------------------------";
    4.18 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    4.19 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    4.20 +"----------- check 'type xlist' {||1, 2, 3||} --------------------------------";
    4.21  (* ML representation *)
    4.22 -val t1 = @{term "[|| ||]"};
    4.23 -val t2 = @{term "[||1,2,3||]"};
    4.24 +val t1 = @{term "{|| ||}"};
    4.25 +val t2 = @{term "{||1,2,3||}"};
    4.26  
    4.27  (* pretty printing *)
    4.28  if Print_Mode.setmp [] 
    4.29    (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t1
    4.30 -  = "[|| ||]"
    4.31 -then () else error "CHANGED pretty printing of '[|| ||]'";
    4.32 +  = "{|| ||}"
    4.33 +then () else error "CHANGED pretty printing of '{|| ||}'";
    4.34  
    4.35  if Print_Mode.setmp [] 
    4.36    (Syntax.string_of_term (Config.put show_markup false (Proof_Context.init_global @{theory}))) t2
    4.37 -  = "[||1::'a, 2::'a, 3::'a||]"
    4.38 -then () else error "CHANGED pretty printing of '[||1,2,3||]'"
    4.39 +  = "{|| 1::'a, 2::'a, 3::'a ||}"
    4.40 +then () else error "CHANGED pretty printing of '{||1,2,3||}'"
    4.41  
    4.42  (* parsing *)
    4.43 -Syntax.read_term_global @{theory} "[|| ||]";
    4.44 -Syntax.read_term_global @{theory} "[||1,2,3||]";
    4.45 +Syntax.read_term_global @{theory} "{|| ||}";
    4.46 +Syntax.read_term_global @{theory} "{||1,2,3||}";
    4.47  
    4.48  "--------------------- NTH ---------------------------------------------------";
    4.49  "--------------------- NTH ---------------------------------------------------";