# HG changeset patch # User wenzelm # Date 1126018793 -7200 # Node ID f27456a2a975658868fe8bc822a29a5abab98297 # Parent ab45d65bf2044b0e60a5fd8a90e032c22cc20544 converted to Isar theory format; diff -r ab45d65bf204 -r f27456a2a975 src/HOL/Hoare/Arith2.ML --- a/src/HOL/Hoare/Arith2.ML Tue Sep 06 16:59:52 2005 +0200 +++ b/src/HOL/Hoare/Arith2.ML Tue Sep 06 16:59:53 2005 +0200 @@ -6,12 +6,8 @@ More arithmetic lemmas. *) -open Arith2; - - (*** cd ***) - Goalw [cd_def] "0 cd n n n"; by (Asm_simp_tac 1); qed "cd_nnn"; @@ -42,7 +38,7 @@ by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1); qed "gcd_nnn"; -val prems = goalw thy [gcd_def] "gcd m n = gcd n m"; +val prems = goalw (the_context ()) [gcd_def] "gcd m n = gcd n m"; by (simp_tac (simpset() addsimps [cd_swap]) 1); qed "gcd_swap"; diff -r ab45d65bf204 -r f27456a2a975 src/HOL/Hoare/Arith2.thy --- a/src/HOL/Hoare/Arith2.thy Tue Sep 06 16:59:52 2005 +0200 +++ b/src/HOL/Hoare/Arith2.thy Tue Sep 06 16:59:53 2005 +0200 @@ -6,19 +6,23 @@ More arithmetic. Much of this duplicates ex/Primes. *) -Arith2 = Main + +theory Arith2 +imports Main +begin constdefs - cd :: [nat, nat, nat] => bool + "cd" :: "[nat, nat, nat] => bool" "cd x m n == x dvd m & x dvd n" - gcd :: [nat, nat] => nat + gcd :: "[nat, nat] => nat" "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)" -consts fac :: nat => nat +consts fac :: "nat => nat" primrec "fac 0 = Suc 0" "fac(Suc n) = (Suc n)*fac(n)" +ML {* use_legacy_bindings (the_context ()) *} + end