# HG changeset patch
# User wenzelm
# Date 1464449668 -7200
# Node ID 878bd5922f3b9eea9aadb5c49f5e14f74f18310f
# Parent  d4f459eb7ed044715abc2106885050acfda16193
clarified axiomatization: proper variables (!);

diff -r d4f459eb7ed0 -r 878bd5922f3b src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Fri May 27 23:58:24 2016 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Sat May 28 17:34:28 2016 +0200
@@ -15,12 +15,29 @@
   append_name :: mname
 
 axiomatization val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam :: vnam
-where distinct_fields: "val_name \<noteq> next_name"
-  and distinct_vars:
-  "l_nam \<noteq> l1_nam" "l_nam \<noteq> l2_nam" "l_nam \<noteq> l3_nam" "l_nam \<noteq> l4_nam"
-  "l1_nam \<noteq> l2_nam" "l1_nam \<noteq> l3_nam" "l1_nam \<noteq> l4_nam"
-  "l2_nam \<noteq> l3_nam" "l2_nam \<noteq> l4_nam"
-  "l3_nam \<noteq> l4_nam"
+where distinct_fields: "val_nam \<noteq> next_nam"
+  and distinct_vars1: "l_nam \<noteq> l1_nam"
+  and distinct_vars2: "l_nam \<noteq> l2_nam"
+  and distinct_vars3: "l_nam \<noteq> l3_nam"
+  and distinct_vars4: "l_nam \<noteq> l4_nam"
+  and distinct_vars5: "l1_nam \<noteq> l2_nam"
+  and distinct_vars6: "l1_nam \<noteq> l3_nam"
+  and distinct_vars7: "l1_nam \<noteq> l4_nam"
+  and distinct_vars8: "l2_nam \<noteq> l3_nam"
+  and distinct_vars9: "l2_nam \<noteq> l4_nam"
+  and distinct_vars10: "l3_nam \<noteq> l4_nam"
+
+lemmas distinct_vars =
+  distinct_vars1
+  distinct_vars2
+  distinct_vars3
+  distinct_vars4
+  distinct_vars5
+  distinct_vars6
+  distinct_vars7
+  distinct_vars8
+  distinct_vars9
+  distinct_vars10
 
 definition list_name :: cname where
   "list_name = Cname list_nam"