1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Mon Apr 19 20:44:18 2021 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Tue Apr 20 16:58:44 2021 +0200
1.3 @@ -16,7 +16,7 @@
1.4
1.5 subsection \<open>Power re-defined for a specific type\<close>
1.6 consts
1.7 - pow :: "[real, real] => real" (infixr "^^^" 80)
1.8 + pow :: "[real, real] => real" (infixr "\<up>" 80)
1.9
1.10 subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
1.11 consts
1.12 @@ -138,49 +138,49 @@
1.13 | eval_matches _ _ _ _ = NONE;
1.14 (*
1.15 > val t = (Thm.term_of o the o (parse thy))
1.16 - "matches (?x = 0) (1 * x ^^^ 2 = 0)";
1.17 + "matches (?x = 0) (1 * x \<up> 2 = 0)";
1.18 > eval_matches "/thmid/" "/op_/" t thy;
1.19 val it =
1.20 SOME
1.21 - ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",
1.22 + ("matches (x = 0) (1 * x \<up> 2 = 0) = False",
1.23 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.24
1.25 > val t = (Thm.term_of o the o (parse thy))
1.26 - "matches (?a = #0) (#1 * x ^^^ #2 = #0)";
1.27 + "matches (?a = #0) (#1 * x \<up> #2 = #0)";
1.28 > eval_matches "/thmid/" "/op_/" t thy;
1.29 val it =
1.30 SOME
1.31 - ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",
1.32 + ("matches (?a = #0) (#1 * x \<up> #2 = #0) = True",
1.33 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.34
1.35 > val t = (Thm.term_of o the o (parse thy))
1.36 - "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";
1.37 + "matches (?a * x = #0) (#1 * x \<up> #2 = #0)";
1.38 > eval_matches "/thmid/" "/op_/" t thy;
1.39 val it =
1.40 SOME
1.41 - ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",
1.42 + ("matches (?a * x = #0) (#1 * x \<up> #2 = #0) = False",
1.43 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.44
1.45 > val t = (Thm.term_of o the o (parse thy))
1.46 - "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";
1.47 + "matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0)";
1.48 > eval_matches "/thmid/" "/op_/" t thy;
1.49 val it =
1.50 SOME
1.51 - ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",
1.52 + ("matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0) = True",
1.53 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
1.54 ----- before ?patterns ---:
1.55 > val t = (Thm.term_of o the o (parse thy))
1.56 "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
1.57 > eval_matches "/thmid/" "/op_/" t thy;
1.58 SOME
1.59 - ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",
1.60 + ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1) = True",
1.61 Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
1.62 : (string * term) option
1.63
1.64 > val t = (Thm.term_of o the o (parse thy))
1.65 "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
1.66 > eval_matches "/thmid/" "/op_/" t thy;
1.67 -SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",
1.68 +SOME ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1) = False",
1.69 Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
1.70
1.71 > val t = (Thm.term_of o the o (parse thy))
1.72 @@ -233,11 +233,11 @@
1.73 HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
1.74 | eval_lhs _ _ _ _ = NONE;
1.75 (*
1.76 -> val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";
1.77 +> val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x \<up> 2 = 0)";
1.78 > val SOME (id,t') = eval_lhs 0 0 t 0;
1.79 -val id = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
1.80 +val id = "Prog_Expr.lhs (1 * x \<up> 2 = 0) = 1 * x \<up> 2" : string
1.81 > term2str t';
1.82 -val it = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
1.83 +val it = "Prog_Expr.lhs (1 * x \<up> 2 = 0) = 1 * x \<up> 2" : string
1.84 *)
1.85
1.86 fun rhs (Const ("HOL.eq",_) $ _ $ r) = r