equal
deleted
inserted
replaced
804 (** initialize the interpreter state used by the 'me' **) |
804 (** initialize the interpreter state used by the 'me' **) |
805 val (t, _, revsets, _) = ini t; |
805 val (t, _, revsets, _) = ini t; |
806 |
806 |
807 if length (hd revsets) = 11 then () else error "length of revset changed"; |
807 if length (hd revsets) = 11 then () else error "length of revset changed"; |
808 if (revsets |> nth 1 |> nth 1 |> id_of_thm) = |
808 if (revsets |> nth 1 |> nth 1 |> id_of_thm) = |
809 (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.thmID_of_derivation_name) |
809 (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id) |
810 then () else error "first element of revset changed"; |
810 then () else error "first element of revset changed"; |
811 if |
811 if |
812 (revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\",?r1 ^^^ 2 = ?r1 * ?r1)" andalso |
812 (revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\",?r1 ^^^ 2 = ?r1 * ?r1)" andalso |
813 (revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 ^^^ 2\",9 = 3 ^^^ 2)" andalso |
813 (revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 ^^^ 2\",9 = 3 ^^^ 2)" andalso |
814 (revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\",6 * x = 2 * (3 * x))" |
814 (revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\",6 * x = 2 * (3 * x))" |