equal
deleted
inserted
replaced
892 ]) |
892 ]) |
893 *} |
893 *} |
894 |
894 |
895 |
895 |
896 |
896 |
897 (****************************************) |
897 |
898 (* cleaning of the theorem *) |
898 section {* Cleaning of the theorem *} |
899 (****************************************) |
|
900 |
|
901 |
|
902 |
899 |
903 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *) |
900 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *) |
904 ML {* |
901 ML {* |
905 fun exchange_ty lthy rty qty ty = |
902 fun exchange_ty lthy rty qty ty = |
906 let |
903 let |