diff -r 89a2ff3f82c7 -r df05cd030d2f IntEx.thy --- a/IntEx.thy Wed Oct 28 10:29:00 2009 +0100 +++ b/IntEx.thy Wed Oct 28 15:25:11 2009 +0100 @@ -12,27 +12,17 @@ apply(auto simp add: mem_def expand_fun_eq) done -print_quotients - -typ my_int +quotient_def (for my_int) + ZERO::"my_int" +where + "ZERO \ (0::nat, 0::nat)" -local_setup {* - make_const_def @{binding "ZERO"} @{term "(0::nat, 0::nat)"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd -*} - -term ZERO thm ZERO_def -(* -quotient_def (with my_int) - ZERO :: "my_int" +quotient_def (for my_int) + ONE::"my_int" where - "ZERO \ (0::nat, 0::nat)" -*) - -local_setup {* - make_const_def @{binding ONE} @{term "(1::nat, 0::nat)"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd -*} + "ONE \ (1::nat, 0::nat)" term ONE thm ONE_def @@ -42,9 +32,10 @@ where "my_plus (x, y) (u, v) = (x + u, y + v)" -local_setup {* - make_const_def @{binding PLUS} @{term "my_plus"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd -*} +quotient_def (for my_int) + PLUS::"my_int \ my_int \ my_int" +where + "PLUS \ my_plus" term PLUS thm PLUS_def @@ -55,7 +46,7 @@ "my_neg (x, y) = (y, x)" local_setup {* - make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd + old_make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd *} term NEG @@ -72,7 +63,7 @@ "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" local_setup {* - make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd + old_make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd *} term MULT @@ -85,7 +76,7 @@ "my_le (x, y) (u, v) = (x+v \ u+y)" local_setup {* - make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd + old_make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \ nat"} @{typ "my_int"} #> snd *} term LE