Trac189.thy « isar « etc - proof-general - Emacs interface for proof assistants

about summary refs log tree commit diff homepage

path: root/etc/isar/Trac189.thy

blob: 43c4bdd430f249facf2fabe19a556fc1320b0b2c (plain)

theory Trac189 imports Main begin


(* Undoing of a diagnostic: exercises proof-no-command *)

lemma "True"
  apply (rule TrueI)
  thm TrueI