equal
deleted
inserted
replaced
1 (* Title: quick and dirty for quick update Isabelle2002 --> Isabelle2009-2 |
1 (* Title: quick and dirty for quick update Isabelle2002 --> Isabelle2009-2 |
2 Author: Walther Neuper 000301 |
2 Author: Walther Neuper 000301 |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 *) |
4 *) |
5 |
5 |
6 theory Delete imports "../ProgLang/Language" begin |
6 theory Delete imports "../ProgLang/ProgLang" begin |
7 |
7 |
8 axioms (* theorems which are available only with long names, |
8 axioms (* theorems which are available only with long names, |
9 which can not yet be handled in isac's scripts *) |
9 which can not yet be handled in isac's scripts *) |
10 |
10 |
11 real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)" |
11 real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)" |