--- a/src/LCF/ex/Ex3.thy Sat Sep 03 17:54:07 2005 +0200
+++ b/src/LCF/ex/Ex3.thy Sat Sep 03 17:54:10 2005 +0200
@@ -1,14 +1,20 @@
-(*** Addition with fixpoint of successor ***)
+(* $Id$ *)
+
+header {* Addition with fixpoint of successor *}
-Ex3 = LCF +
+theory Ex3
+imports LCF
+begin
consts
- s :: "'a => 'a"
- p :: "'a => 'a => 'a"
+ s :: "'a => 'a"
+ p :: "'a => 'a => 'a"
-rules
- p_strict "p(UU) = UU"
- p_s "p(s(x),y) = s(p(x,y))"
+axioms
+ p_strict: "p(UU) = UU"
+ p_s: "p(s(x),y) = s(p(x,y))"
+
+ML {* use_legacy_bindings (the_context ()) *}
end