equal
deleted
inserted
replaced
398 done |
398 done |
399 |
399 |
400 lemma Compl_Collect: "- Collect b = {x. \<not> b x}" |
400 lemma Compl_Collect: "- Collect b = {x. \<not> b x}" |
401 by blast |
401 by blast |
402 |
402 |
403 lemmas AbortRule = SkipRule \<comment> "dummy version" |
403 lemmas AbortRule = SkipRule \<comment> \<open>dummy version\<close> |
404 |
404 |
405 ML_file "~~/src/HOL/Hoare/hoare_tac.ML" |
405 ML_file "~~/src/HOL/Hoare/hoare_tac.ML" |
406 |
406 |
407 method_setup hoare = |
407 method_setup hoare = |
408 \<open>Scan.succeed (fn ctxt => |
408 \<open>Scan.succeed (fn ctxt => |