equal
deleted
inserted
replaced
38 |
38 |
39 val (p,_,f,nxt,_,pt) = me nxt p''' [] pt'''; (*nxt = Check_elementwise "Assumptions"*) |
39 val (p,_,f,nxt,_,pt) = me nxt p''' [] pt'''; (*nxt = Check_elementwise "Assumptions"*) |
40 case nxt of (Check_elementwise "Assumptions") => () |
40 case nxt of (Check_elementwise "Assumptions") => () |
41 | _ => error "Check_elementwise changed; after switch sub-->root-method"; |
41 | _ => error "Check_elementwise changed; after switch sub-->root-method"; |
42 |
42 |
|
43 (*ctxt*)Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*) |