src/Tools/isac/Isac_Protocol.thy
changeset 59346 bf5ca91db537
parent 59260 0161ef48c8cc
child 59390 f6374c995ac5
equal deleted inserted replaced
59345:425c687ec4c3 59346:bf5ca91db537
     1 theory Isac_Protocol
     1 theory Isac_Protocol
     2 imports "~~/libisabelle-protocol/protocol/Protocol" "~~/src/Tools/isac/Knowledge/Build_Thydata"
     2 imports "~~/libisabelle-protocol/libisabelle/protocol/Protocol" "~~/src/Tools/isac/Knowledge/Build_Thydata"
     3 begin
     3 begin
     4 
     4 
     5 (* val appendFormula : calcID -> cterm' -> XML.tree *)
     5 (* val appendFormula : calcID -> cterm' -> XML.tree *)
     6 operation_setup (sequential, bracket, auto) append_form = 
     6 operation_setup (sequential, bracket, auto) append_form = 
     7   \<open>fn intree => 
     7   \<open>fn intree =>