declare recursive equation as ".simps", in accordance with other packages
authorkrauss
Tue, 26 Oct 2010 12:19:01 +0200
changeset 40169 11ea439d947f
parent 40166 d3bc972b7d9d
child 40170 751121d5ca35
declare recursive equation as ".simps", in accordance with other packages
src/HOL/Tools/Function/partial_function.ML
src/HOL/ex/Fundefs.thy
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Oct 26 12:19:01 2010 +0200
@@ -218,7 +218,7 @@
     lthy'
     |> Local_Theory.note (eq_abinding, [rec_rule])
     |-> (fn (_, rec') =>
-      Local_Theory.note ((Binding.qualify true fname (Binding.name "rec"), []), rec'))
+      Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec'))
     |> snd
   end;
 
--- a/src/HOL/ex/Fundefs.thy	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/ex/Fundefs.thy	Tue Oct 26 12:19:01 2010 +0200
@@ -222,7 +222,7 @@
      then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
      else do { ns \<leftarrow> collatz (3 * n + 1);  Some (n # ns)})"
 
-declare collatz.rec[code]
+declare collatz.simps[code]
 value "collatz 23"