1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Sep 29 19:34:32 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue Nov 16 18:26:57 2021 +0100
     1.3 @@ -92,22 +92,6 @@
     1.4  	        | _ => ls @ [o1, o2])
     1.5          | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])
     1.6      in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end
     1.7 -(*>val t = @{term True};
     1.8 -> val t' = or2list t;
     1.9 -> term2str t';
    1.10 -"ListC.UniversalList"
    1.11 -> val t = @{term False};
    1.12 -> val t' = or2list t;
    1.13 -> term2str t';
    1.14 -"[]"
    1.15 -> val t=(Thm.term_of o the o (parse thy)) "x=3";
    1.16 -> val t' = or2list t;
    1.17 -> term2str t';
    1.18 -"[x = 3]"
    1.19 -> val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
    1.20 -> val t' = or2list t;
    1.21 -> term2str t';
    1.22 -"[x = #3, x = #-3, x = #0]" : string *)
    1.23  
    1.24  
    1.25  (** evaluation on the meta-level **)
    1.26 @@ -125,58 +109,6 @@
    1.27          val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
    1.28  	    in SOME (UnparseC.term_in_thy thy prop, prop) end
    1.29    | eval_matches _ _ _ _ = NONE; 
    1.30 -(*
    1.31 -> val t  = (Thm.term_of o the o (parse thy)) 
    1.32 -	      "matches (?x = 0) (1 * x \<up> 2 = 0)";
    1.33 -> eval_matches "/thmid/" "/op_/" t thy;
    1.34 -val it =
    1.35 -  SOME
    1.36 -    ("matches (x = 0) (1 * x \<up> 2 = 0) = False",
    1.37 -     Const (#,#) $ (# $ # $ Const #)) : (string * term) option
    1.38 -
    1.39 -> val t  = (Thm.term_of o the o (parse thy)) 
    1.40 -	      "matches (?a = #0) (#1 * x \<up> #2 = #0)";
    1.41 -> eval_matches "/thmid/" "/op_/" t thy;
    1.42 -val it =
    1.43 -  SOME
    1.44 -    ("matches (?a = #0) (#1 * x \<up> #2 = #0) = True",
    1.45 -     Const (#,#) $ (# $ # $ Const #)) : (string * term) option
    1.46 -
    1.47 -> val t  = (Thm.term_of o the o (parse thy)) 
    1.48 -	      "matches (?a * x = #0) (#1 * x \<up> #2 = #0)";
    1.49 -> eval_matches "/thmid/" "/op_/" t thy;
    1.50 -val it =
    1.51 -  SOME
    1.52 -    ("matches (?a * x = #0) (#1 * x \<up> #2 = #0) = False",
    1.53 -     Const (#,#) $ (# $ # $ Const #)) : (string * term) option
    1.54 -
    1.55 -> val t  = (Thm.term_of o the o (parse thy)) 
    1.56 -	      "matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0)";
    1.57 -> eval_matches "/thmid/" "/op_/" t thy;
    1.58 -val it =
    1.59 -  SOME
    1.60 -    ("matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0) = True",
    1.61 -     Const (#,#) $ (# $ # $ Const #)) : (string * term) option                  
    1.62 ------ before ?patterns ---:
    1.63 -> val t  = (Thm.term_of o the o (parse thy)) 
    1.64 -	      "matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1)";
    1.65 -> eval_matches "/thmid/" "/op_/" t thy;
    1.66 -SOME
    1.67 -    ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1) = True",
    1.68 -     Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
    1.69 -  : (string * term) option 
    1.70 -
    1.71 -> val t = (Thm.term_of o the o (parse thy)) 
    1.72 -	      "matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1)";
    1.73 -> eval_matches "/thmid/" "/op_/" t thy;
    1.74 -SOME ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1) = False",
    1.75 -     Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
    1.76 -
    1.77 -> val t = (Thm.term_of o the o (parse thy)) 
    1.78 -               "matches (a = b) (x + #1 + #-1 * #2 = #0)";
    1.79 -> eval_matches "/thmid/" "/op_/" t thy;
    1.80 -SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
    1.81 -*)
    1.82  
    1.83  (*.does a pattern match some subterm ?.*)
    1.84  fun matchsub thy t pat =