ProgTutorial/Parsing.thy
changeset 546 d84867127c5d
parent 544 501491d56798
child 553 c53d74b34123
equal deleted inserted replaced
545:4a1539a2c18e 546:d84867127c5d
  1511 lemma "True"
  1511 lemma "True"
  1512 apply(test)
  1512 apply(test)
  1513 oops
  1513 oops
  1514 
  1514 
  1515 method_setup joker = {* 
  1515 method_setup joker = {* 
  1516   Scan.lift (Scan.succeed (fn ctxt => Method.cheating true)) *} {* bla *}
  1516   Scan.lift (Scan.succeed (fn ctxt => Method.cheating ctxt true)) *} {* bla *}
  1517 
  1517 
  1518 lemma "False"
  1518 lemma "False"
  1519 apply(joker)
  1519 apply(joker)
  1520 oops
  1520 oops
  1521 
  1521