equal
deleted
inserted
replaced
69 VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn] |
69 VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn] |
70 **) |
70 **) |
71 fun get_vars c = |
71 fun get_vars c = |
72 let |
72 let |
73 val d = Logic.strip_assums_concl c; |
73 val d = Logic.strip_assums_concl c; |
74 val Const _ $ pre $ _ $ _ $ _ = HOLogic.dest_Trueprop d; |
74 val pre = |
|
75 case HOLogic.dest_Trueprop d of |
|
76 Const _ $ pre $ _ $ _ $ _ => pre |
|
77 | Const _ $ pre $ _ $ _ => pre \<comment> \<open>support for \<^file>\<open>~~/src/HOL/Isar_Examples/Hoare.thy\<close>\<close> |
75 in mk_vars pre end; |
78 in mk_vars pre end; |
76 |
79 |
77 fun mk_CollectC tm = |
80 fun mk_CollectC tm = |
78 let val \<^Type>\<open>fun t _\<close> = fastype_of tm; |
81 let val \<^Type>\<open>fun t _\<close> = fastype_of tm; |
79 in \<^Const>\<open>Collect t for tm\<close> end; |
82 in \<^Const>\<open>Collect t for tm\<close> end; |