# HG changeset patch
# User nipkow
# Date 1101120848 -3600
# Node ID 51f3d31e8eeaa0dabecd8564781b46492a81118d
# Parent  0bd9eedaa3016f5544dd36617b0ca998676b451e
fixed proof

diff -r 0bd9eedaa301 -r 51f3d31e8eea src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Mon Nov 22 11:53:56 2004 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Mon Nov 22 11:54:08 2004 +0100
@@ -371,8 +371,6 @@
   {((Class Base, Class Base), [Class Base])}"
 apply (unfold appl_methds_def)
 apply (simp (no_asm))
-apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
-apply  (auto simp add: map_of_Cons foo_Base_def)
 done
 
 lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) =  
diff -r 0bd9eedaa301 -r 51f3d31e8eea src/HOL/ex/mesontest2.ML
--- a/src/HOL/ex/mesontest2.ML	Mon Nov 22 11:53:56 2004 +0100
+++ b/src/HOL/ex/mesontest2.ML	Mon Nov 22 11:54:08 2004 +0100
@@ -1382,9 +1382,9 @@
 \  (\\<forall>Xr X Y. equal(intersection(cross_product(X::'a,Y),Xr),restrct(Xr::'a,X,Y))) &    \
 \  (\\<forall>Z X. ~(equal(restrct(X::'a,singleton(Z),universal_class),null_class) & member(Z::'a,domain_of(X)))) &    \
 \  (\\<forall>Z X. member(Z::'a,universal_class) --> equal(restrct(X::'a,singleton(Z),universal_class),null_class) | member(Z::'a,domain_of(X))) &        \
-\  (\\<forall>X. subclass(rotate(X),cross_product(cross_product(universal_class::'a,universal_class),universal_class))) &   \
-\  (\\<forall>V W U X. member(ordered_pair(ordered_pair(U::'a,V),W),rotate(X)) --> member(ordered_pair(ordered_pair(V::'a,W),U),X)) &   \
-\  (\\<forall>U V W X. member(ordered_pair(ordered_pair(V::'a,W),U),X) & member(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> member(ordered_pair(ordered_pair(U::'a,V),W),rotate(X))) & \
+\  (\\<forall>X. subclass(rot(X),cross_product(cross_product(universal_class::'a,universal_class),universal_class))) &   \
+\  (\\<forall>V W U X. member(ordered_pair(ordered_pair(U::'a,V),W),rot(X)) --> member(ordered_pair(ordered_pair(V::'a,W),U),X)) &   \
+\  (\\<forall>U V W X. member(ordered_pair(ordered_pair(V::'a,W),U),X) & member(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> member(ordered_pair(ordered_pair(U::'a,V),W),rot(X))) & \
 \  (\\<forall>X. subclass(flip(X),cross_product(cross_product(universal_class::'a,universal_class),universal_class))) &     \
 \  (\\<forall>V U W X. member(ordered_pair(ordered_pair(U::'a,V),W),flip(X)) --> member(ordered_pair(ordered_pair(V::'a,U),W),X)) &     \
 \  (\\<forall>U V W X. member(ordered_pair(ordered_pair(V::'a,U),W),X) & member(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> member(ordered_pair(ordered_pair(U::'a,V),W),flip(X))) &   \
@@ -1485,7 +1485,7 @@
 \  (\\<forall>P4 Q4 R4 S4. equal(P4::'a,Q4) --> equal(restrct(P4::'a,R4,S4),restrct(Q4::'a,R4,S4))) &     \
 \  (\\<forall>T4 V4 U4 W4. equal(T4::'a,U4) --> equal(restrct(V4::'a,T4,W4),restrct(V4::'a,U4,W4))) &     \
 \  (\\<forall>X4 Z4 A5 Y4. equal(X4::'a,Y4) --> equal(restrct(Z4::'a,A5,X4),restrct(Z4::'a,A5,Y4))) &     \
-\  (\\<forall>B5 C5. equal(B5::'a,C5) --> equal(rotate(B5),rotate(C5))) &   \
+\  (\\<forall>B5 C5. equal(B5::'a,C5) --> equal(rot(B5),rot(C5))) &   \
 \  (\\<forall>D5 E5. equal(D5::'a,E5) --> equal(second(D5),second(E5))) &   \
 \  (\\<forall>F5 G5. equal(F5::'a,G5) --> equal(singleton(F5),singleton(G5))) &     \
 \  (\\<forall>H5 I5. equal(H5::'a,I5) --> equal(successor(H5),successor(I5))) &     \
@@ -2308,12 +2308,12 @@
 \  (\\<forall>X Z. member(Z::'a,inv1 X) --> ordered_pair_predicate(Z)) &       \
 \  (\\<forall>Z X. member(Z::'a,inv1 X) --> member(ordered_pair(second(Z),first(Z)),X)) &      \
 \  (\\<forall>Z X. little_set(Z) & ordered_pair_predicate(Z) & member(ordered_pair(second(Z),first(Z)),X) --> member(Z::'a,inv1 X)) &  \
-\  (\\<forall>Z X. member(Z::'a,rotate_right(X)) --> little_set(f9(Z::'a,X))) & \
-\  (\\<forall>Z X. member(Z::'a,rotate_right(X)) --> little_set(f10(Z::'a,X))) &        \
-\  (\\<forall>Z X. member(Z::'a,rotate_right(X)) --> little_set(f11(Z::'a,X))) &        \
-\  (\\<forall>Z X. member(Z::'a,rotate_right(X)) --> equal(Z::'a,ordered_pair(f9(Z::'a,X),ordered_pair(f10(Z::'a,X),f11(Z::'a,X))))) &      \
-\  (\\<forall>Z X. member(Z::'a,rotate_right(X)) --> member(ordered_pair(f10(Z::'a,X),ordered_pair(f11(Z::'a,X),f9(Z::'a,X))),X)) &     \
-\  (\\<forall>Z V W U X. little_set(Z) & little_set(U) & little_set(V) & little_set(W) & equal(Z::'a,ordered_pair(U::'a,ordered_pair(V::'a,W))) & member(ordered_pair(V::'a,ordered_pair(W::'a,U)),X) --> member(Z::'a,rotate_right(X))) &      \
+\  (\\<forall>Z X. member(Z::'a,rot_right(X)) --> little_set(f9(Z::'a,X))) & \
+\  (\\<forall>Z X. member(Z::'a,rot_right(X)) --> little_set(f10(Z::'a,X))) &        \
+\  (\\<forall>Z X. member(Z::'a,rot_right(X)) --> little_set(f11(Z::'a,X))) &        \
+\  (\\<forall>Z X. member(Z::'a,rot_right(X)) --> equal(Z::'a,ordered_pair(f9(Z::'a,X),ordered_pair(f10(Z::'a,X),f11(Z::'a,X))))) &      \
+\  (\\<forall>Z X. member(Z::'a,rot_right(X)) --> member(ordered_pair(f10(Z::'a,X),ordered_pair(f11(Z::'a,X),f9(Z::'a,X))),X)) &     \
+\  (\\<forall>Z V W U X. little_set(Z) & little_set(U) & little_set(V) & little_set(W) & equal(Z::'a,ordered_pair(U::'a,ordered_pair(V::'a,W))) & member(ordered_pair(V::'a,ordered_pair(W::'a,U)),X) --> member(Z::'a,rot_right(X))) &      \
 \  (\\<forall>Z X. member(Z::'a,flip_range_of(X)) --> little_set(f12(Z::'a,X))) &       \
 \  (\\<forall>Z X. member(Z::'a,flip_range_of(X)) --> little_set(f13(Z::'a,X))) &       \
 \  (\\<forall>Z X. member(Z::'a,flip_range_of(X)) --> little_set(f14(Z::'a,X))) &       \
@@ -2496,7 +2496,7 @@
 \  (\\<forall>S11 T11. equal(S11::'a,T11) --> equal(range_of(S11),range_of(T11))) & \
 \  (\\<forall>U11 V11 W11. equal(U11::'a,V11) --> equal(restrct(U11::'a,W11),restrct(V11::'a,W11))) &     \
 \  (\\<forall>X11 Z11 Y11. equal(X11::'a,Y11) --> equal(restrct(Z11::'a,X11),restrct(Z11::'a,Y11))) &     \
-\  (\\<forall>A12 B12. equal(A12::'a,B12) --> equal(rotate_right(A12),rotate_right(B12))) & \
+\  (\\<forall>A12 B12. equal(A12::'a,B12) --> equal(rot_right(A12),rot_right(B12))) & \
 \  (\\<forall>C12 D12. equal(C12::'a,D12) --> equal(second(C12),second(D12))) &     \
 \  (\\<forall>K12 L12. equal(K12::'a,L12) --> equal(sigma(K12),sigma(L12))) &       \
 \  (\\<forall>M12 N12. equal(M12::'a,N12) --> equal(singleton_set(M12),singleton_set(N12))) &       \
diff -r 0bd9eedaa301 -r 51f3d31e8eea src/HOL/ex/set.thy
--- a/src/HOL/ex/set.thy	Mon Nov 22 11:53:56 2004 +0100
+++ b/src/HOL/ex/set.thy	Mon Nov 22 11:54:08 2004 +0100
@@ -108,7 +108,7 @@
   apply (rule bij_if_then_else)
      apply (rule_tac [4] refl)
     apply (rule_tac [2] inj_on_inv)
-    apply (erule subset_inj_on [OF subset_UNIV])
+    apply (erule subset_inj_on [OF _ subset_UNIV])
    txt {* Tricky variable instantiations! *}
    apply (erule ssubst, subst double_complement)
    apply (rule subsetI, erule imageE, erule ssubst, rule rangeI)