1.1 --- a/src/Tools/isac/Interpret/mstools.sml Fri Mar 04 11:30:37 2011 +0100
1.2 +++ b/src/Tools/isac/Interpret/mstools.sml Fri Mar 04 11:43:45 2011 +0100
1.3 @@ -593,7 +593,7 @@
1.4 if is_list v
1.5 then [v] (*eg. [r=Arbfix]*)
1.6 else (case v of (*eg. eps=#0*)
1.7 - (Const ("op =",_) $ l $ r) => [r,l]
1.8 + (Const ("HOL.eq",_) $ l $ r) => [r,l]
1.9 | _ =>
1.10 error ("pbl_ids Tools.nam: no equality "
1.11 ^ Print_Mode.setmp [] (Syntax.string_of_term ctxt) v))
1.12 @@ -640,7 +640,7 @@
1.13 (case vs of
1.14 [] => error ("pbl_ids' Tools.nam called with []")
1.15 | [t] => (case t of (*eg. eps=#0*)
1.16 - (Const ("op =",_) $ l $ r) => [r,l]
1.17 + (Const ("HOL.eq",_) $ l $ r) => [r,l]
1.18 | _ =>
1.19 error ("pbl_ids' Tools.nam: no equality " ^ term2str t))
1.20 | vs' => vs (*14.9.01: ???TODO *))
2.1 --- a/src/Tools/isac/Interpret/script.sml Fri Mar 04 11:30:37 2011 +0100
2.2 +++ b/src/Tools/isac/Interpret/script.sml Fri Mar 04 11:43:45 2011 +0100
2.3 @@ -303,7 +303,7 @@
2.4 "una" => [t]
2.5 | "nam" =>
2.6 [case t of
2.7 - r as (Const ("op =",_) $ _ $ _) => r
2.8 + r as (Const ("HOL.eq",_) $ _ $ _) => r
2.9 | _ => error ("mk_arg: dsc-typ 'nam' applied to non-equality "^
2.10 (Print_Mode.setmp [] (Syntax.string_of_term
2.11 (thy2ctxt thy)) t))]
3.1 --- a/src/Tools/isac/Knowledge/Atools.thy Fri Mar 04 11:30:37 2011 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Fri Mar 04 11:43:45 2011 +0100
3.3 @@ -372,8 +372,8 @@
3.4
3.5 (*.evaluate identity of terms, which stay ready for evaluation in turn;
3.6 thus returns False only for atoms.*)
3.7 -(*("equal" ,("op =",eval_equal "#equal_")):calc*)
3.8 -fun eval_equal (thmid : string) "op =" (t as
3.9 +(*("equal" ,("HOL.eq",eval_equal "#equal_")):calc*)
3.10 +fun eval_equal (thmid : string) "HOL.eq" (t as
3.11 (Const (op0,t0) $ t1 $ t2 )) thy =
3.12 if t1 = t2
3.13 then SOME (mk_thmid thmid op0
3.14 @@ -466,7 +466,7 @@
3.15 fun eval_sameFunId _ "Atools.sameFunId"
3.16 (p as Const ("Atools.sameFunId",_) $
3.17 (f1 $ _) $
3.18 - (Const ("op =", _) $ (f2 $ _) $ _)) _ =
3.19 + (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
3.20 if f1 = f2
3.21 then SOME ((term2str p) ^ " = True",
3.22 Trueprop $ (mk_equality (p, HOLogic.true_const)))
3.23 @@ -479,7 +479,7 @@
3.24 filter the elements with the same fun-identfier in "f y"
3.25 as the fst argument;
3.26 this is, because Isabelles filter takes more than 1 sec.*)
3.27 -fun same_funid f1 (Const ("op =", _) $ (f2 $ _) $ _) = f1 = f2
3.28 +fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
3.29 | same_funid f1 t = error ("same_funid called with t = ("
3.30 ^term2str f1^") ("^term2str t^")");
3.31 (*("filter_sameFunId" ,("Atools.filter'_sameFunId",
3.32 @@ -541,7 +541,7 @@
3.33 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
3.34 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
3.35 Calc ("Atools.ident",eval_ident "#ident_"),
3.36 - Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*)
3.37 + Calc ("HOL.eq",eval_equal "#equal_"),(*atom <> atom -> False*)
3.38
3.39 Calc ("Tools.Vars",eval_var "#Vars_"),
3.40
3.41 @@ -564,7 +564,7 @@
3.42 append_rls "calculate_Atools" e_rls
3.43 [Calc ("Orderings.ord_class.less",eval_equ "#less_"),
3.44 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
3.45 - Calc ("op =",eval_equal "#equal_"),
3.46 + Calc ("HOL.eq",eval_equal "#equal_"),
3.47
3.48 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
3.49 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
3.50 @@ -574,7 +574,7 @@
3.51
3.52 val Atools_erls =
3.53 append_rls "Atools_erls" e_rls
3.54 - [Calc ("op =",eval_equal "#equal_"),
3.55 + [Calc ("HOL.eq",eval_equal "#equal_"),
3.56 Thm ("not_true",num_str @{thm not_true}),
3.57 (*"(~ True) = False"*)
3.58 Thm ("not_false",num_str @{thm not_false}),
3.59 @@ -606,7 +606,7 @@
3.60
3.61 val Atools_crls =
3.62 append_rls "Atools_crls" e_rls
3.63 - [Calc ("op =",eval_equal "#equal_"),
3.64 + [Calc ("HOL.eq",eval_equal "#equal_"),
3.65 Thm ("not_true",num_str @{thm not_true}),
3.66 Thm ("not_false",num_str @{thm not_false}),
3.67 Thm ("and_true",num_str @{thm and_true}),
3.68 @@ -683,7 +683,7 @@
3.69 ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
3.70 ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_")),
3.71 ("ident" ,("Atools.ident",eval_ident "#ident_")),
3.72 - ("equal" ,("op =",eval_equal "#equal_")),
3.73 + ("equal" ,("HOL.eq",eval_equal "#equal_")),
3.74 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
3.75 ("MINUS" ,("Groups.minus_class.minus",eval_binop "#sub_")),
3.76 ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
4.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Fri Mar 04 11:30:37 2011 +0100
4.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri Mar 04 11:43:45 2011 +0100
4.3 @@ -463,7 +463,7 @@
4.4 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
4.5 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
4.6 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
4.7 - Calc ("op =",eval_equal "#equal_")
4.8 + Calc ("HOL.eq",eval_equal "#equal_")
4.9 ],
4.10 SOME "solveSystem e_s v_s",
4.11 []));
4.12 @@ -502,7 +502,7 @@
4.13 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
4.14 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
4.15 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
4.16 - Calc ("op =",eval_equal "#equal_")
4.17 + Calc ("HOL.eq",eval_equal "#equal_")
4.18 ],
4.19 SOME "solveSystem e_s v_s",
4.20 []));
4.21 @@ -518,7 +518,7 @@
4.22 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
4.23 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
4.24 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
4.25 - Calc ("op =",eval_equal "#equal_")
4.26 + Calc ("HOL.eq",eval_equal "#equal_")
4.27 ],
4.28 SOME "solveSystem e_s v_s",
4.29 []));
5.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Fri Mar 04 11:30:37 2011 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Fri Mar 04 11:43:45 2011 +0100
5.3 @@ -89,8 +89,8 @@
5.4 this is _not in_ the term, because only applied to _whole_ term*)
5.5 fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) =
5.6 let val p' = case p of
5.7 - Const ("op =", T) $ lh $ rh =>
5.8 - Const ("op =", T) $ lh $ mk_add rh (new_c rh)
5.9 + Const ("HOL.eq", T) $ lh $ rh =>
5.10 + Const ("HOL.eq", T) $ lh $ mk_add rh (new_c rh)
5.11 | p => mk_add p (new_c p)
5.12 in SOME ((term2str p) ^ " = " ^ term2str p',
5.13 Trueprop $ (mk_equality (p, p')))
6.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Fri Mar 04 11:30:37 2011 +0100
6.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Fri Mar 04 11:43:45 2011 +0100
6.3 @@ -34,7 +34,7 @@
6.4
6.5 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
6.6 append_rls "LinEq_prls" e_rls
6.7 - [Calc ("op =",eval_equal "#equal_"),
6.8 + [Calc ("HOL.eq",eval_equal "#equal_"),
6.9 Calc ("Tools.matches",eval_matches ""),
6.10 Calc ("Tools.lhs" ,eval_lhs ""),
6.11 Calc ("Tools.rhs" ,eval_rhs ""),
7.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri Mar 04 11:30:37 2011 +0100
7.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri Mar 04 11:43:45 2011 +0100
7.3 @@ -397,7 +397,7 @@
7.4 (*.for evaluation of conditions in rewrite rules.*)
7.5 val Poly_erls =
7.6 append_rls "Poly_erls" Atools_erls
7.7 - [ Calc ("op =",eval_equal "#equal_"),
7.8 + [ Calc ("HOL.eq",eval_equal "#equal_"),
7.9 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
7.10 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
7.11 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
7.12 @@ -407,7 +407,7 @@
7.13
7.14 val poly_crls =
7.15 append_rls "poly_crls" Atools_crls
7.16 - [ Calc ("op =",eval_equal "#equal_"),
7.17 + [ Calc ("HOL.eq",eval_equal "#equal_"),
7.18 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
7.19 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
7.20 Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
8.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Fri Mar 04 11:30:37 2011 +0100
8.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Fri Mar 04 11:43:45 2011 +0100
8.3 @@ -378,7 +378,7 @@
8.4 Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
8.5 (*Calc ("Atools.occurs'_in",eval_occurs_in ""), *)
8.6 (*Calc ("Atools.is'_const",eval_const "#is_const_"),*)
8.7 - Calc ("op =",eval_equal "#equal_"),
8.8 + Calc ("HOL.eq",eval_equal "#equal_"),
8.9 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
8.10 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
8.11 Thm ("not_true",num_str @{thm not_true}),
8.12 @@ -392,7 +392,7 @@
8.13 val PolyEq_erls =
8.14 merge_rls "PolyEq_erls" LinEq_erls
8.15 (append_rls "ops_preds" calculate_Rational
8.16 - [Calc ("op =",eval_equal "#equal_"),
8.17 + [Calc ("HOL.eq",eval_equal "#equal_"),
8.18 Thm ("plus_leq", num_str @{thm plus_leq}),
8.19 Thm ("minus_leq", num_str @{thm minus_leq}),
8.20 Thm ("rat_leq1", num_str @{thm rat_leq1}),
8.21 @@ -403,7 +403,7 @@
8.22 val PolyEq_crls =
8.23 merge_rls "PolyEq_crls" LinEq_crls
8.24 (append_rls "ops_preds" calculate_Rational
8.25 - [Calc ("op =",eval_equal "#equal_"),
8.26 + [Calc ("HOL.eq",eval_equal "#equal_"),
8.27 Thm ("plus_leq", num_str @{thm plus_leq}),
8.28 Thm ("minus_leq", num_str @{thm minus_leq}),
8.29 Thm ("rat_leq1", num_str @{thm rat_leq1}),
9.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Fri Mar 04 11:30:37 2011 +0100
9.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Fri Mar 04 11:43:45 2011 +0100
9.3 @@ -78,7 +78,7 @@
9.4 Calc ("Tools.lhs" ,eval_lhs ""),
9.5 Calc ("Tools.rhs" ,eval_rhs ""),
9.6 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
9.7 - Calc ("op =",eval_equal "#equal_"),
9.8 + Calc ("HOL.eq",eval_equal "#equal_"),
9.9 Thm ("not_true",num_str @{thm not_true}),
9.10 Thm ("not_false",num_str @{thm not_false}),
9.11 Thm ("and_true",num_str @{thm and_true}),
10.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri Mar 04 11:30:37 2011 +0100
10.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Mar 04 11:43:45 2011 +0100
10.3 @@ -1915,7 +1915,7 @@
10.4 (
10.5 Const ("Not",[bool]--->bool) $
10.6 (
10.7 - Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $
10.8 + Const("HOL.eq",[HOLogic.realT,HOLogic.realT]--->bool) $
10.9 poly2term((!p3),vars) $
10.10 Free("0",HOLogic.realT)
10.11 )
10.12 @@ -1945,7 +1945,7 @@
10.13 (
10.14 Const ("Not",[bool]--->bool) $
10.15 (
10.16 - Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $
10.17 + Const("HOL.eq",[HOLogic.realT,HOLogic.realT]--->bool) $
10.18 poly2term((!p3),vars) $
10.19 Free("0",HOLogic.realT)
10.20 )
10.21 @@ -2000,7 +2000,7 @@
10.22 (
10.23 Const ("Not",[bool]--->bool) $
10.24 (
10.25 - Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $
10.26 + Const("HOL.eq",[HOLogic.realT,HOLogic.realT]--->bool) $
10.27 poly2expanded((!p3),vars) $
10.28 Free("0",HOLogic.realT)
10.29 )
10.30 @@ -2030,7 +2030,7 @@
10.31 (
10.32 Const ("Not",[bool]--->bool) $
10.33 (
10.34 - Const("op =",[HOLogic.realT,HOLogic.realT]--->bool) $
10.35 + Const("HOL.eq",[HOLogic.realT,HOLogic.realT]--->bool) $
10.36 poly2expanded((!p3),vars) $
10.37 Free("0",HOLogic.realT)
10.38 )
10.39 @@ -2767,7 +2767,7 @@
10.40 Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
10.41 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [], *)
10.42 rules =
10.43 - [Calc ("op =",eval_equal "#equal_"),
10.44 + [Calc ("HOL.eq",eval_equal "#equal_"),
10.45 Calc ("Atools.is'_const",eval_const "#is_const_"),
10.46 Thm ("not_true",num_str @{thm not_true}),
10.47 Thm ("not_false",num_str @{thm not_false})
11.1 --- a/src/Tools/isac/Knowledge/Root.thy Fri Mar 04 11:30:37 2011 +0100
11.2 +++ b/src/Tools/isac/Knowledge/Root.thy Fri Mar 04 11:43:45 2011 +0100
11.3 @@ -172,7 +172,7 @@
11.4 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
11.5 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
11.6 Calc ("Groups.times_class.times", eval_binop "#mult_"),
11.7 - Calc ("op =",eval_equal "#equal_")
11.8 + Calc ("HOL.eq",eval_equal "#equal_")
11.9 ];
11.10
11.11 val Root_erls =
11.12 @@ -184,7 +184,7 @@
11.13 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
11.14 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
11.15 Calc ("Groups.times_class.times", eval_binop "#mult_"),
11.16 - Calc ("op =",eval_equal "#equal_")
11.17 + Calc ("HOL.eq",eval_equal "#equal_")
11.18 ];
11.19
11.20 ruleset' := overwritelthy @{theory} (!ruleset',
12.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Fri Mar 04 11:30:37 2011 +0100
12.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Fri Mar 04 11:43:45 2011 +0100
12.3 @@ -205,7 +205,7 @@
12.4 Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""),
12.5 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
12.6 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
12.7 - Calc ("op =",eval_equal "#equal_"),
12.8 + Calc ("HOL.eq",eval_equal "#equal_"),
12.9 Thm ("not_true",num_str @{thm not_true}),
12.10 Thm ("not_false",num_str @{thm not_false}),
12.11 Thm ("and_true",num_str @{thm and_true}),
13.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Fri Mar 04 11:30:37 2011 +0100
13.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Fri Mar 04 11:43:45 2011 +0100
13.3 @@ -80,7 +80,7 @@
13.4 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
13.5 Calc ("RootRatEq.is'_rootRatAddTerm'_in",
13.6 eval_is_rootRatAddTerm_in ""),
13.7 - Calc ("op =",eval_equal "#equal_"),
13.8 + Calc ("HOL.eq",eval_equal "#equal_"),
13.9 Thm ("not_true",num_str @{thm not_true}),
13.10 Thm ("not_false",num_str @{thm not_false}),
13.11 Thm ("and_true",num_str @{thm and_true}),
14.1 --- a/src/Tools/isac/Knowledge/Test.thy Fri Mar 04 11:30:37 2011 +0100
14.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Mar 04 11:43:45 2011 +0100
14.3 @@ -655,17 +655,17 @@
14.4
14.5
14.6 exception NO_EQUATION_TERM;
14.7 -fun is_equation ((Const ("op =",(Type ("fun",
14.8 +fun is_equation ((Const ("HOL.eq",(Type ("fun",
14.9 [Type (_,[]),Type ("fun",
14.10 [Type (_,[]),Type ("bool",[])])])))) $ _ $ _)
14.11 = true
14.12 | is_equation _ = false;
14.13 -fun equ_lhs ((Const ("op =",(Type ("fun",
14.14 +fun equ_lhs ((Const ("HOL.eq",(Type ("fun",
14.15 [Type (_,[]),Type ("fun",
14.16 [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
14.17 = l
14.18 | equ_lhs _ = raise NO_EQUATION_TERM;
14.19 -fun equ_rhs ((Const ("op =",(Type ("fun",
14.20 +fun equ_rhs ((Const ("HOL.eq",(Type ("fun",
14.21 [Type (_,[]),Type ("fun",
14.22 [Type (_,[]),Type ("bool",[])])])))) $ l $ r)
14.23 = r
15.1 --- a/src/Tools/isac/ProgLang/Tools.thy Fri Mar 04 11:30:37 2011 +0100
15.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Fri Mar 04 11:43:45 2011 +0100
15.3 @@ -60,7 +60,7 @@
15.4 (*+ for Or_to_List +*)
15.5 fun or2list (Const ("True",_)) = (tracing"### or2list True";UniversalList)
15.6 | or2list (Const ("False",_)) = (tracing"### or2list False";EmptyList)
15.7 - | or2list (t as Const ("op =",_) $ _ $ _) =
15.8 + | or2list (t as Const ("HOL.eq",_) $ _ $ _) =
15.9 (tracing"### or2list _ = _";list2isalist bool [t])
15.10 | or2list ors =
15.11 (tracing"### or2list _ | _";
15.12 @@ -192,11 +192,11 @@
15.13 in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
15.14 | eval_var _ _ _ _ = NONE;
15.15
15.16 -fun lhs (Const ("op =",_) $ l $ _) = l
15.17 +fun lhs (Const ("HOL.eq",_) $ l $ _) = l
15.18 | lhs t = error("lhs called with (" ^ term2str t ^ ")");
15.19 (*("lhs" ,("Tools.lhs" ,eval_lhs "")):calc*)
15.20 fun eval_lhs _ "Tools.lhs"
15.21 - (t as (Const ("Tools.lhs",_) $ (Const ("op =",_) $ l $ _))) _ =
15.22 + (t as (Const ("Tools.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =
15.23 SOME ((term2str t) ^ " = " ^ (term2str l),
15.24 Trueprop $ (mk_equality (t, l)))
15.25 | eval_lhs _ _ _ _ = NONE;
15.26 @@ -208,11 +208,11 @@
15.27 val it = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
15.28 *)
15.29
15.30 -fun rhs (Const ("op =",_) $ _ $ r) = r
15.31 +fun rhs (Const ("HOL.eq",_) $ _ $ r) = r
15.32 | rhs t = error("rhs called with (" ^ term2str t ^ ")");
15.33 (*("rhs" ,("Tools.rhs" ,eval_rhs "")):calc*)
15.34 fun eval_rhs _ "Tools.rhs"
15.35 - (t as (Const ("Tools.rhs",_) $ (Const ("op =",_) $ _ $ r))) _ =
15.36 + (t as (Const ("Tools.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =
15.37 SOME ((term2str t) ^ " = " ^ (term2str r),
15.38 Trueprop $ (mk_equality (t, r)))
15.39 | eval_rhs _ _ _ _ = NONE;
16.1 --- a/src/Tools/isac/ProgLang/termC.sml Fri Mar 04 11:30:37 2011 +0100
16.2 +++ b/src/Tools/isac/ProgLang/termC.sml Fri Mar 04 11:43:45 2011 +0100
16.3 @@ -326,15 +326,15 @@
16.4
16.5
16.6
16.7 -fun dest_equals' (Const("op =",_) $ t $ u) = (t,u)(* logic.ML: Const("=="*)
16.8 +fun dest_equals' (Const("HOL.eq",_) $ t $ u) = (t,u)(* logic.ML: Const("=="*)
16.9 | dest_equals' t = raise TERM("dest_equals'", [t]);
16.10 val lhs_ = (fst o dest_equals');
16.11 val rhs_ = (snd o dest_equals');
16.12
16.13 -fun is_equality (Const("op =",_) $ t $ u) = true (* logic.ML: Const("=="*)
16.14 +fun is_equality (Const("HOL.eq",_) $ t $ u) = true (* logic.ML: Const("=="*)
16.15 | is_equality _ = false;
16.16 -fun mk_equality (t,u) = (Const("op =",[type_of t,type_of u]--->bool) $ t $ u);
16.17 -fun is_expliceq (Const("op =",_) $ (Free _) $ u) = true
16.18 +fun mk_equality (t,u) = (Const("HOL.eq",[type_of t,type_of u]--->bool) $ t $ u);
16.19 +fun is_expliceq (Const("HOL.eq",_) $ (Free _) $ u) = true
16.20 | is_expliceq _ = false;
16.21 fun strip_trueprop (Const("Trueprop",_) $ t) = t
16.22 | strip_trueprop t = t;
17.1 --- a/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML Fri Mar 04 11:30:37 2011 +0100
17.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/2interpreter/2foointerpreter.ML Fri Mar 04 11:43:45 2011 +0100
17.3 @@ -8,7 +8,7 @@
17.4 "fooprog (a = b)";
17.5 (*val trm =
17.6 Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $
17.7 - (Const ("op =", "'a => 'a => bool") $ Free ("a", "'a") $
17.8 + (Const ("HOL.eq", "'a => 'a => bool") $ Free ("a", "'a") $
17.9 Free ("b", "'a"))
17.10 : term*)
17.11 foointerpret trm;
18.1 --- a/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy Fri Mar 04 11:30:37 2011 +0100
18.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy Fri Mar 04 11:43:45 2011 +0100
18.3 @@ -48,7 +48,7 @@
18.4 val trm = Syntax.read_term_global @{theory Foo_Know111}
18.5 "fooprog (foo222 = bar222)";
18.6 (*Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $
18.7 - (Const ("op =", "'a => 'a => bool") $ Free ("foo222", "'a") $
18.8 + (Const ("HOL.eq", "'a => 'a => bool") $ Free ("foo222", "'a") $
18.9 Free ("bar222", "'a"))
18.10 : term*)
18.11
18.12 @@ -56,7 +56,7 @@
18.13 "fooprog (foo111 = bar111)";
18.14 (*val trm =
18.15 Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $
18.16 - (Const ("op =", "'a => 'a => bool") $ Free ("foo111", "'a") $
18.17 + (Const ("HOL.eq", "'a => 'a => bool") $ Free ("foo111", "'a") $
18.18 Free ("bar111", "'a"))
18.19 : term*)
18.20 *}
19.1 --- a/test/Tools/isac/Interpret/calchead.sml Fri Mar 04 11:30:37 2011 +0100
19.2 +++ b/test/Tools/isac/Interpret/calchead.sml Fri Mar 04 11:43:45 2011 +0100
19.3 @@ -513,7 +513,7 @@
19.4
19.5 case match_ags thy PATS AGS of
19.6 [(1, [1], "#Given", Const ("Descript.equality", _),
19.7 - [Const ("op =", _) $ (Const ("Groups.plus_class.plus", _) $
19.8 + [Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $
19.9 Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]),
19.10 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]),
19.11 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])]
20.1 --- a/test/Tools/isac/Interpret/script.sml Fri Mar 04 11:30:37 2011 +0100
20.2 +++ b/test/Tools/isac/Interpret/script.sml Fri Mar 04 11:43:45 2011 +0100
20.3 @@ -177,7 +177,7 @@
20.4 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
20.5 trace_rewrite:=false;
20.6 (*Exception TYPE raised:
20.7 -Illegal type for constant "op =" :: "[real, bool] => bool"
20.8 +Illegal type for constant "HOL.eq" :: "[real, bool] => bool"
20.9 Atools.argument'_in (Tools.lhs (ListG.nth_ (1 + -1 + -1) [])) =
20.10 ListG.nth_ (1 + -1 + -1) []
20.11 Exception-
20.12 @@ -185,7 +185,7 @@
20.13 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
20.14 [],
20.15 [Const ("Trueprop", "bool => prop") $
20.16 - (Const ("op =", "[RealDef.real, bool] => bool") $ ... $ ...)])
20.17 + (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
20.18 raised
20.19 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
20.20 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
21.1 --- a/test/Tools/isac/Knowledge/atools.sml Fri Mar 04 11:30:37 2011 +0100
21.2 +++ b/test/Tools/isac/Knowledge/atools.sml Fri Mar 04 11:43:45 2011 +0100
21.3 @@ -63,11 +63,11 @@
21.4 "----------- sameFunId -------------------------------------------";
21.5 val t = str2term "M_b L"; atomty t;
21.6 val t as f1 $ _ = str2term "M_b L";
21.7 -val t as Const ("op =", _) $ (f2 $ _) $ _ = str2term "M_b x = c + L*x";
21.8 +val t as Const ("HOL.eq", _) $ (f2 $ _) $ _ = str2term "M_b x = c + L*x";
21.9 f1 = f2 (*true*);
21.10 val (p as Const ("Atools.sameFunId",_) $
21.11 (f1 $ _) $
21.12 - (Const ("op =", _) $ (f2 $ _) $ _)) =
21.13 + (Const ("HOL.eq", _) $ (f2 $ _) $ _)) =
21.14 str2term "sameFunId (M_b L) (M_b x = c + L*x)";
21.15 f1 = f2 (*true*);
21.16 eval_sameFunId "" "Atools.sameFunId"
22.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Fri Mar 04 11:30:37 2011 +0100
22.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Fri Mar 04 11:43:45 2011 +0100
22.3 @@ -89,7 +89,7 @@
22.4 [(Thm ("length_Nil_",num_str @{thm length_Nil_})),
22.5 (Thm ("length_Cons_",num_str @{thm length_Cons_})),
22.6 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
22.7 - Calc ("op =",eval_equal "#equal_")
22.8 + Calc ("HOL.eq",eval_equal "#equal_")
22.9 ];
22.10 val SOME (t',_) = rewrite_set_ thy false testrls t;
22.11 if term2str t' = "True" then ()
23.1 --- a/test/Tools/isac/Knowledge/poly.sml Fri Mar 04 11:30:37 2011 +0100
23.2 +++ b/test/Tools/isac/Knowledge/poly.sml Fri Mar 04 11:43:45 2011 +0100
23.3 @@ -185,7 +185,7 @@
23.4 val tm = str2term "(5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) + (-48 * x ^^^ 4 + 8))) is_multUnordered";
23.5 case eval_is_multUnordered "testid" "" tm thy of
23.6 SOME (_, Const ("Trueprop", _) $
23.7 - (Const ("op =", _) $
23.8 + (Const ("HOL.eq", _) $
23.9 (Const ("Poly.is'_multUnordered", _) $ _) $
23.10 Const ("True", _))) => ()
23.11 | _ => error "poly.sml diff. eval_is_multUnordered";
24.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Fri Mar 04 11:30:37 2011 +0100
24.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Fri Mar 04 11:43:45 2011 +0100
24.3 @@ -180,7 +180,7 @@
24.4 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
24.5 (Logic.count_prems r', [], r'));
24.6 case p' of
24.7 - [Const ("Not", _) $ (Const ("op =", _) $ Free ("y", _) $
24.8 + [Const ("Not", _) $ (Const ("HOL.eq", _) $ Free ("y", _) $
24.9 Const ("Groups.zero_class.zero", _))] => ()
24.10 | _ => error "rewrite.sml assumption changed";
24.11 "=====^^^ make asms without Trueprop ---^^^";
24.12 @@ -441,7 +441,7 @@
24.13 val tm = str2term "(x^^^2 * x) is_multUnordered";
24.14 case eval_is_multUnordered "testid" "" tm thy of
24.15 SOME (_, Const ("Trueprop", _) $
24.16 - (Const ("op =", _) $
24.17 + (Const ("HOL.eq", _) $
24.18 (Const ("Poly.is'_multUnordered", _) $ _) $
24.19 Const ("True", _))) => ()
24.20 | _ => error "rewrite.sml diff. eval_is_multUnordered 2";