Simplified primrec definitions.

--- a/src/HOL/List.thy	Fri Aug 02 12:14:49 1996 +0200
+++ b/src/HOL/List.thy	Fri Aug 02 12:16:11 1996 +0200
@@ -47,45 +47,45 @@
   "Alls x:xs.P" == "list_all (%x.P) xs"
 
 primrec hd list
-  hd_Nil  "hd([]) = (@x.False)"
-  hd_Cons "hd(x#xs) = x"
+  "hd([]) = (@x.False)"
+  "hd(x#xs) = x"
 primrec tl list
-  tl_Nil  "tl([]) = (@x.False)"
-  tl_Cons "tl(x#xs) = xs"
+  "tl([]) = (@x.False)"
+  "tl(x#xs) = xs"
 primrec ttl list
   (* a "total" version of tl: *)
-  ttl_Nil  "ttl([]) = []"
-  ttl_Cons "ttl(x#xs) = xs"
+  "ttl([]) = []"
+  "ttl(x#xs) = xs"
 primrec "op mem" list
-  mem_Nil  "x mem [] = False"
-  mem_Cons "x mem (y#ys) = (if y=x then True else x mem ys)"
+  "x mem [] = False"
+  "x mem (y#ys) = (if y=x then True else x mem ys)"
 primrec setOfList list
-  setOfList_Nil  "setOfList [] = {}"
-  setOfList_Cons "setOfList (x#xs) = insert x (setOfList xs)"
+  "setOfList [] = {}"
+  "setOfList (x#xs) = insert x (setOfList xs)"
 primrec list_all list
   list_all_Nil  "list_all P [] = True"
   list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
 primrec map list
-  map_Nil  "map f [] = []"
-  map_Cons "map f (x#xs) = f(x)#map f xs"
+  "map f [] = []"
+  "map f (x#xs) = f(x)#map f xs"
 primrec "op @" list
-  append_Nil  "[] @ ys = ys"
-  append_Cons "(x#xs)@ys = x#(xs@ys)"
+  "[] @ ys = ys"
+  "(x#xs)@ys = x#(xs@ys)"
 primrec rev list
-  rev_Nil  "rev([]) = []"
-  rev_Cons "rev(x#xs) = rev(xs) @ [x]"
+  "rev([]) = []"
+  "rev(x#xs) = rev(xs) @ [x]"
 primrec filter list
-  filter_Nil  "filter P [] = []"
-  filter_Cons "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
+  "filter P [] = []"
+  "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
 primrec foldl list
-  foldl_Nil  "foldl f a [] = a"
-  foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
+  "foldl f a [] = a"
+  "foldl f a (x#xs) = foldl f (f a x) xs"
 primrec length list
-  length_Nil  "length([]) = 0"
-  length_Cons "length(x#xs) = Suc(length(xs))"
+  "length([]) = 0"
+  "length(x#xs) = Suc(length(xs))"
 primrec flat list
-  flat_Nil  "flat([]) = []"
-  flat_Cons "flat(x#xs) = x @ flat(xs)"
+  "flat([]) = []"
+  "flat(x#xs) = x @ flat(xs)"
 primrec drop list
   drop_Nil  "drop n [] = []"
   drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
@@ -95,3 +95,4 @@
 defs
   nth_def  "nth(n) == nat_rec hd (%m r xs. r(tl(xs))) n"
 end
+

--- a/src/HOL/ex/PropLog.thy	Fri Aug 02 12:14:49 1996 +0200
+++ b/src/HOL/ex/PropLog.thy	Fri Aug 02 12:16:11 1996 +0200
@@ -33,13 +33,14 @@
   eval_def "tt[p] == eval2 p tt"
 
 primrec eval2 pl
-  eval2_false "eval2(false) = (%x.False)"
-  eval2_var   "eval2(#v) = (%tt.v:tt)"
-  eval2_imp   "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)"
+  "eval2(false) = (%x.False)"
+  "eval2(#v) = (%tt.v:tt)"
+  "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)"
 
 primrec hyps pl
-  hyps_false "hyps(false) = (%tt.{})"
-  hyps_var   "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
-  hyps_imp   "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)"
+  "hyps(false) = (%tt.{})"
+  "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
+  "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)"
 
 end
+