--- a/NEWS Tue Sep 28 15:21:45 2010 +0200
+++ b/NEWS Tue Sep 28 15:34:47 2010 +0200
@@ -74,10 +74,12 @@
*** HOL ***
+* Dropped old primrec package. INCOMPATIBILITY.
+
* Improved infrastructure for term evaluation using code generator
techniques, in particular static evaluation conversions.
-* String.literal is a type, but not a datatype. INCOMPATIBILITY.
+* String.literal is a type, but not a datatype. INCOMPATIBILITY.
* Renamed lemmas:
expand_fun_eq -> fun_eq_iff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SET_Protocol/SET_Protocol.thy Tue Sep 28 15:34:47 2010 +0200
@@ -0,0 +1,12 @@
+(* Title: HOL/SET_Protocol/SET_Protocol.thy
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2003 University of Cambridge
+
+Root file for the SET protocol proofs.
+*)
+
+theory SET_Protocol
+imports Cardholder_Registration Merchant_Registration Purchase
+begin
+
+end
--- a/src/HOL/Tools/primrec.ML Tue Sep 28 15:21:45 2010 +0200
+++ b/src/HOL/Tools/primrec.ML Tue Sep 28 15:34:47 2010 +0200
@@ -320,12 +320,7 @@
val _ =
Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
Keyword.thy_decl
- ((primrec_decl >> (fn ((opt_target, fixes), specs) =>
- Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
- || (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
- Toplevel.theory (snd o
- (if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec)
- alt_name (map Parse.triple_swap eqns) o
- tap (fn _ => legacy_feature "Old variant of 'primrec' command -- use new syntax instead")))));
+ (primrec_decl >> (fn ((opt_target, fixes), specs) =>
+ Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)));
end;