# HG changeset patch
# User haftmann
# Date 1286196408 -7200
# Node ID 8c83139a14331eb1d85ec009ebcb7db502589458
# Parent  ecf97cf3d248be0cd5bac50f378fd38b938e75b7
turned distinct and sorted into inductive predicates: yields nice induction principles for free

diff -r ecf97cf3d248 -r 8c83139a1433 NEWS
--- a/NEWS	Mon Oct 04 12:22:58 2010 +0200
+++ b/NEWS	Mon Oct 04 14:46:48 2010 +0200
@@ -74,6 +74,10 @@
 
 *** HOL ***
 
+* Predicates `distinct` and `sorted` now defined inductively, with nice
+induction rules.  INCOMPATIBILITY: former distinct.simps and sorted.simps
+now named distinct_simps and sorted_simps.
+
 * Constant `contents` renamed to `the_elem`, to free the generic name
 contents for other uses.  INCOMPATIBILITY.
 
diff -r ecf97cf3d248 -r 8c83139a1433 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Mon Oct 04 12:22:58 2010 +0200
+++ b/src/HOL/Library/Permutation.thy	Mon Oct 04 14:46:48 2010 +0200
@@ -168,7 +168,7 @@
     apply simp
     apply (subgoal_tac "a#list <~~> a#ysa@zs")
      apply (metis Cons_eq_appendI perm_append_Cons trans)
-    apply (metis Cons Cons_eq_appendI distinct.simps(2)
+    apply (metis Cons Cons_eq_appendI distinct_simps(2)
       distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
    apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
     apply (fastsimp simp add: insert_ident)